The full Mordell–Lang conjecture for abelian varieties over function fields

Let $p$ be a prime, let $k$ be a finite field of characteristic $p$, let $K/k$ be a regular extension with algebraic closure $K\subseteq\overline K$, and let $A$ be a $K$-abelian variety. Let $X\subseteq A_{\overline K}$ be an irreducible $\overline K$-subvariety and let $\Gamma\subseteq A(\overline K)$ be a finite-rank subgroup, meaning that $\Gamma\otimes_{\mathbb{Z}}\mathbb{Q}$ has finite dimension over $\mathbb{Q}$. Assume that $X(\overline K)\cap\Gamma$ is Zariski dense in $X$. The full Mordell–Lang conjecture. Then there exist an abelian variety $A_0$ over $\overline{\mathbb{F}}_p\subseteq\overline K$, an $\overline{\mathbb{F}}_p$-subvariety $X_0\subseteq A_0$, a surjective morphism $h:A\rightarrow A_0\times_{\overline{\mathbb{F}}_p}K$, and an $x\in A(\overline K)$ such that

$$X=x+h^{-1}(X_0).$$

This is the full Mordell–Lang statement recalled as motivation for the paper. In the source it is stated as a conjecture and is reported to be proved by Hrushovski in the important case where $\Gamma\otimes\mathbb{Z}_p$ is a finitely generated $\mathbb{Z}_p$-module; accordingly, its database status is solved.