[proofplan] Choose a bijection from the independent basis $I$ to the independent basis $J$ and make it fix $A$ pointwise; since independence over $A$ is understood relative to $D \setminus A$, there is no conflict on $A \cap I$ or $A \cap J$. The hypothesis on finite independent tuples says that every finite part of this bijection is an [elementary map](/page/Elementary%20Map) over $A$. We then extend finite elementary maps by using the atomicity of prime models over their bases: each element of $M_I$ has a type isolated over $A$ together with finitely many elements of $I$, and the isolating formula can be transported along the corresponding finite part of the bijection. The same extension argument works in both directions, giving a back-and-forth system whose union is an isomorphism fixing $A$ pointwise. [/proofplan]

[step:Choose a basis bijection whose finite restrictions are elementary over $A$]Since $|I|=|J|$, choose a bijection \begin{align*} f_0:I &\to J. \end{align*} Here $I$ and $J$ are [independent](/page/Independence) subsets of the $A$-definable [strongly minimal set](/page/Strongly%20Minimal%20Set) $D$, so independence over $A$ is taken in $D \setminus A$. Thus $I \cap A=\varnothing$ and $J \cap A=\varnothing$, and there is no ambiguity in extending $f_0$ to $A \cup I$ by requiring $f_0(a)=a$ for every $a \in A$. Let $i_1,\dots,i_n \in I$ be distinct elements, where $n \in \mathbb{N}$. Since $I$ is independent over $A$, the tuple $(i_1,\dots,i_n)$ is independent over $A$. Since $f_0$ is injective and $J$ is independent over $A$, the tuple $(f_0(i_1),\dots,f_0(i_n))$ is also independent over $A$. By the hypothesis on finite independent tuples, \begin{align*} \operatorname{tp}(i_1,\dots,i_n/A) = \operatorname{tp}(f_0(i_1),\dots,f_0(i_n)/A). \end{align*} Here $\operatorname{tp}(\cdot/A)$ denotes the complete [type](/page/Type) over $A$. Thus every finite restriction of $f_0$ is elementary over $A$.[/step]

[guided]We first build the map on the independent bases, because the bases are the only non-model-theoretic data distinguishing $M_I$ from $M_J$. Since $I$ and $J$ have the same cardinality, there is a bijection \begin{align*} f_0:I &\to J. \end{align*} The sets $I$ and $J$ are [independent](/page/Independence) subsets of the $A$-definable [strongly minimal set](/page/Strongly%20Minimal%20Set) $D$, so independence over $A$ is being taken in $D \setminus A$. Hence $I \cap A=\varnothing$ and $J \cap A=\varnothing$. We may therefore extend this map to $A \cup I$ without any conflict by declaring that it fixes the parameter set $A$ pointwise: for every $a \in A$, set $f_0(a)=a$. The point of the hypothesis on finite independent tuples is precisely that this arbitrary bijection is already elementary on finite pieces. Let $i_1,\dots,i_n \in I$ be distinct, with $n \in \mathbb{N}$. Because $I$ is independent over $A$, the tuple $(i_1,\dots,i_n)$ is independent over $A$. Because $f_0$ is injective and its image lies in the independent set $J$, the tuple $(f_0(i_1),\dots,f_0(i_n))$ is also independent over $A$. The assumption therefore gives \begin{align*} \operatorname{tp}(i_1,\dots,i_n/A) = \operatorname{tp}(f_0(i_1),\dots,f_0(i_n)/A). \end{align*} This equality of complete [types](/page/Type) over $A$ says exactly that every formula with parameters from $A$ true of $(i_1,\dots,i_n)$ is true of $(f_0(i_1),\dots,f_0(i_n))$, and conversely. Hence the restriction of $f_0$ to $A \cup \{i_1,\dots,i_n\}$ is an [elementary map](/page/Elementary%20Map) over $A$. Since the finite tuple was arbitrary, every finite restriction of $f_0$ is elementary over $A$.[/guided]

[step:Reduce the problem to uniqueness of prime models over elementarily matched bases]Let $B_I := A \cup I$ and $B_J := A \cup J$. The preceding step proves that the map \begin{align*} f_0:B_I &\to B_J \end{align*} fixing $A$ pointwise and sending each $i \in I$ to $f_0(i) \in J$ is elementary on every finite tuple from $B_I$. Therefore $f_0$ is a partial [elementary map](/page/Elementary%20Map) from $M_I$ to $M_J$ with domain $B_I$ and image $B_J$. By the strengthened hypothesis in the statement, $M_I$ is [prime over](/page/Prime%20Model) and atomic over $B_I$, and $M_J$ is prime and atomic over $B_J$. We use the standard [uniqueness of prime atomic models over elementarily matched bases](/page/Atomic%20Model): if $N_1$ is prime and atomic over $B_1$, $N_2$ is prime and atomic over $B_2$, and $e:B_1 \to B_2$ is elementary, then $e$ extends to an isomorphism $N_1 \cong N_2$. The hypotheses of this result are satisfied with $N_1=M_I$, $N_2=M_J$, $B_1=B_I$, $B_2=B_J$, and $e=f_0$. Applying it gives an isomorphism \begin{align*} F:M_I &\to M_J \end{align*} with $F|_{B_I}=f_0$. Since $f_0(a)=a$ for every $a \in A$, the isomorphism $F$ fixes $A$ pointwise.[/step]

[guided]The earlier proof tried to build finite partial maps directly inside $M_I$ and $M_J$. The difficulty is that a finite elementary map on model elements does not automatically amalgamate with new basis elements from $I$ unless one proves the joint [type](/page/Type) over $A$. The cleaner way is to first regard the entire basis map as a partial elementary map between the parameter sets over which the models are [prime over](/page/Prime%20Model) and atomic. Define \begin{align*} B_I &:= A \cup I, & B_J &:= A \cup J. \end{align*} The map \begin{align*} f_0:B_I &\to B_J \end{align*} is defined by $f_0(a)=a$ for $a \in A$ and by the chosen bijection $I \to J$ on $I$. To check that $f_0$ is elementary, it is enough to check finite tuples, because first-order formulas mention only finitely many parameters. The previous step did exactly this: every finite tuple of distinct elements from $I$ has the same type over $A$ as its image tuple in $J$, and repetitions or entries from $A$ are handled by equality and by the fact that $f_0$ fixes $A$ pointwise. Hence $f_0$ is a partial elementary map with domain $B_I$ and image $B_J$. Now we invoke the [uniqueness of prime atomic models over elementarily matched bases](/page/Atomic%20Model). The property says: if $N_1$ is prime and atomic over $B_1$, $N_2$ is prime and atomic over $B_2$, and $e:B_1 \to B_2$ is elementary, then $e$ extends to an isomorphism $N_1 \cong N_2$. We verify its hypotheses. By the theorem statement, $M_I$ is prime and atomic over $A \cup I=B_I$, and $M_J$ is prime and atomic over $A \cup J=B_J$. The map $f_0:B_I \to B_J$ was proved above to be elementary. Thus, with $B_1=B_I$, $B_2=B_J$, and $e=f_0$, there is an isomorphism \begin{align*} F:M_I &\to M_J \end{align*} such that $F|_{B_I}=f_0$. Since $f_0$ fixes $A$ pointwise, the extension $F$ also fixes $A$ pointwise.[/guided]

[step:Conclude the isomorphism fixes $A$] The isomorphism $F:M_I \to M_J$ obtained in the previous step extends $f_0:B_I \to B_J$. Since $f_0(a)=a$ for every $a \in A$, one has $F(a)=a$ for every $a \in A$. Therefore \begin{align*} M_I \cong_A M_J. \end{align*} This is the required conclusion. [/step]