[proofplan]
We use the standard pregeometry theorem for strongly minimal structures: in a [strongly minimal theory](/page/Strongly%20Minimal%20Theory), [algebraic closure](/page/Algebraic%20Closure) on $M$ satisfies the [pregeometry](/page/Pregeometry) axioms of monotonicity, finite character, idempotence, and exchange. Throughout the proof, write $\operatorname{acl}(S)$ for the algebraic closure in $M$ of a parameter set $S \subseteq M$. We first use [Zorn's lemma](/page/Zorn%27s%20Lemma) to extend any independent set to a maximal independent set over $A$, and then show that maximality forces this set to span $M$ over $A$. Finally, the exchange axiom gives the usual Steinitz replacement argument: finite independent subsets of the closure of a finite independent set have bounded size, and finite character reduces the infinite case to a cardinal-counting union over finite supports.
[/proofplan]
[step:Use Zorn's lemma to extend the independent set to a maximal independent set]
Let $I \subseteq M$ be an independent set over $A$. Let $\mathcal{P}$ be the collection of all subsets $J \subseteq M$ such that $I \subseteq J$ and $J$ is independent over $A$, ordered by inclusion. The set $\mathcal{P}$ is nonempty because $I \in \mathcal{P}$.
Let $\mathcal{C} \subseteq \mathcal{P}$ be a chain, and define
\begin{align*}
J_{\mathcal{C}} := \bigcup_{J \in \mathcal{C}} J.
\end{align*}
We verify that $J_{\mathcal{C}}$ is independent over $A$. Suppose not. Then there are $x \in J_{\mathcal{C}}$ and finitely many distinct elements $x_1,\dots,x_n \in J_{\mathcal{C}} \setminus \{x\}$ such that
\begin{align*}
x \in \operatorname{acl}(A \cup \{x_1,\dots,x_n\}).
\end{align*}
For each $k \in \{1,\dots,n\}$ choose $J_k \in \mathcal{C}$ with $x_k \in J_k$, and choose $J_0 \in \mathcal{C}$ with $x \in J_0$. Since $\mathcal{C}$ is a chain and only finitely many sets $J_0,\dots,J_n$ are involved, one of them contains all the elements $x,x_1,\dots,x_n$. That member of $\mathcal{C}$ is then dependent over $A$, contradicting its membership in $\mathcal{P}$. Hence $J_{\mathcal{C}} \in \mathcal{P}$, so every chain has an upper bound.
By [Zorn's lemma](/page/Zorn%27s%20Lemma), $\mathcal{P}$ has a maximal element. Fix such a maximal element and call it $B$. Then
\begin{align*}
I \subseteq B \subseteq M,
\end{align*}
and $B$ is independent over $A$.
[guided]
Let $I \subseteq M$ be an independent set over $A$. We want a maximal independent extension of $I$, and the natural tool is [Zorn's lemma](/page/Zorn%27s%20Lemma). Define $\mathcal{P}$ to be the collection of all sets $J \subseteq M$ such that $I \subseteq J$ and $J$ is independent over $A$, ordered by inclusion. This partially ordered set is nonempty because $I$ itself is independent over $A$, so $I \in \mathcal{P}$.
To apply [Zorn's lemma](/theorems/1226), every chain must have an upper bound inside $\mathcal{P}$. Let $\mathcal{C} \subseteq \mathcal{P}$ be a chain and define
\begin{align*}
J_{\mathcal{C}} := \bigcup_{J \in \mathcal{C}} J.
\end{align*}
The set $J_{\mathcal{C}}$ contains $I$, so the only point to check is independence over $A$. Suppose $J_{\mathcal{C}}$ were dependent over $A$. By finite character for algebraic closure in the pregeometry, there would exist $x \in J_{\mathcal{C}}$ and finitely many distinct elements $x_1,\dots,x_n \in J_{\mathcal{C}} \setminus \{x\}$ such that
\begin{align*}
x \in \operatorname{acl}(A \cup \{x_1,\dots,x_n\}).
\end{align*}
For each $k \in \{1,\dots,n\}$ choose $J_k \in \mathcal{C}$ with $x_k \in J_k$, and choose $J_0 \in \mathcal{C}$ with $x \in J_0$. Since $\mathcal{C}$ is linearly ordered by inclusion and the list $J_0,\dots,J_n$ is finite, one of these sets contains all the elements $x,x_1,\dots,x_n$. That member of $\mathcal{C}$ would be dependent over $A$, contradicting that every member of $\mathcal{C}$ belongs to $\mathcal{P}$. Hence $J_{\mathcal{C}}$ is independent over $A$, so $J_{\mathcal{C}} \in \mathcal{P}$ and is an upper bound for $\mathcal{C}$.
Therefore the hypotheses of Zorn's lemma are satisfied: $\mathcal{P}$ is nonempty and every chain has an upper bound in $\mathcal{P}$. Zorn's lemma gives a maximal element $B \in \mathcal{P}$. By the definition of $\mathcal{P}$, this means
\begin{align*}
I \subseteq B \subseteq M,
\end{align*}
and $B$ is independent over $A$.
[/guided]
[/step]
[step:Show that maximal independent sets span $M$ over $A$]
We prove that $M \subseteq \operatorname{acl}(A \cup B)$. Let $c \in M$. If $c \in B$, then
\begin{align*}
c \in A \cup B \subseteq \operatorname{acl}(A \cup B),
\end{align*}
so assume $c \notin B$.
If $c \notin \operatorname{acl}(A \cup B)$, then $B \cup \{c\}$ is independent over $A$. To verify this, suppose toward a contradiction that $B \cup \{c\}$ is dependent over $A$. Since $B$ is independent over $A$, any dependence must involve $c$. There are two possible forms.
First, finite character could give a finite set $F \subseteq B$ such that
\begin{align*}
c \in \operatorname{acl}(A \cup F) \subseteq \operatorname{acl}(A \cup B),
\end{align*}
contrary to the assumption. Second, there could be an element $b \in B$ and a finite set $F \subseteq B \setminus \{b\}$ such that
\begin{align*}
b \in \operatorname{acl}(A \cup F \cup \{c\}).
\end{align*}
Because $B$ is independent over $A$, we have
\begin{align*}
b \notin \operatorname{acl}(A \cup F).
\end{align*}
The [exchange axiom for algebraic closure in a strongly minimal theory](/page/Pregeometry), applied over the parameter set $A \cup F$ to $b$ and $c$, gives
\begin{align*}
c \in \operatorname{acl}(A \cup F \cup \{b\}) \subseteq \operatorname{acl}(A \cup B),
\end{align*}
again contradicting the assumption. Hence no dependence exists, so $B \cup \{c\}$ is independent over $A$.
Thus $B \cup \{c\}$ would be an element of $\mathcal{P}$ properly containing $B$, contradicting maximality. Therefore $c \in \operatorname{acl}(A \cup B)$. Since $c \in M$ was arbitrary, $B$ spans $M$ over $A$.
[/step]
[step:Prove the finite Steinitz bound for independent subsets of finite closures]
[claim:Finite Steinitz bound]
For every parameter set $P \subseteq M$, let $E,F \subseteq M$ be finite sets such that $F$ is independent over $P$ and $E$ is independent over $P$. If
\begin{align*}
E \subseteq \operatorname{acl}(P \cup F),
\end{align*}
then $|E| \leq |F|$.
[/claim]
[proof]
We first prove the finite replacement lemma used in the induction. Let $P \subseteq M$, let $X=\{x_1,\dots,x_m\} \subseteq M$ be finite and independent over $P$, and let $y \in \operatorname{acl}(P \cup X) \setminus \operatorname{acl}(P)$. Choose the least $r \in \{1,\dots,m\}$ such that
\begin{align*}
y \in \operatorname{acl}(P \cup \{x_1,\dots,x_r\}).
\end{align*}
Then
\begin{align*}
y \notin \operatorname{acl}(P \cup \{x_1,
\dots,x_{r-1}\}).
\end{align*}
Applying the [exchange axiom for algebraic closure in a strongly minimal theory](/page/Pregeometry) over $P \cup \{x_1,\dots,x_{r-1}\}$ to $y$ and $x_r$ gives
\begin{align*}
x_r \in \operatorname{acl}(P \cup \{x_1,\dots,x_{r-1}\} \cup \{y\})
\subseteq
\operatorname{acl}(P \cup (X \setminus \{x_r\}) \cup \{y\}).
\end{align*}
Since $y \in \operatorname{acl}(P \cup X)$, monotonicity and idempotence give
\begin{align*}
\operatorname{acl}(P \cup X)
=
\operatorname{acl}(P \cup (X \setminus \{x_r\}) \cup \{y\}).
\end{align*}
We also verify that $(X \setminus \{x_r\}) \cup \{y\}$ is independent over $P$. If not, then because $X \setminus \{x_r\}$ is independent over $P$, the dependence must involve $y$. If the dependence is witnessed by $y$, then there is a finite set $H \subseteq X \setminus \{x_r\}$ such that
\begin{align*}
y \in \operatorname{acl}(P \cup H).
\end{align*}
If instead the dependence is witnessed by some $z \in X \setminus \{x_r\}$, then there is a finite set $H \subseteq X \setminus \{x_r,z\}$ such that
\begin{align*}
z \in \operatorname{acl}(P \cup H \cup \{y\}).
\end{align*}
Since $X$ is independent over $P$, we have $z \notin \operatorname{acl}(P \cup H)$. The exchange axiom over $P \cup H$ gives
\begin{align*}
y \in \operatorname{acl}(P \cup H \cup \{z\}) \subseteq \operatorname{acl}(P \cup (X \setminus \{x_r\})).
\end{align*}
Thus in all cases $y \in \operatorname{acl}(P \cup (X \setminus \{x_r\}))$. Combining this with $x_r \in \operatorname{acl}(P \cup \{x_1,\dots,x_{r-1}\} \cup \{y\})$ and using monotonicity and idempotence yields
\begin{align*}
x_r \in \operatorname{acl}(P \cup (X \setminus \{x_r\})),
\end{align*}
contradicting the independence of $X$ over $P$. Thus $(X \setminus \{x_r\}) \cup \{y\}$ is independent over $P$.
We now prove the bound by induction on $|E|$, uniformly in the parameter set $P$. If $E=\varnothing$, then $|E|=0 \leq |F|$. Assume $E \neq \varnothing$, choose $e \in E$, and define $E_0 := E \setminus \{e\}$. Since $E$ is independent over $P$, we have $e \notin \operatorname{acl}(P)$; since $E \subseteq \operatorname{acl}(P \cup F)$, we have $e \in \operatorname{acl}(P \cup F)$. Applying the finite replacement lemma to $X=F$ and $y=e$ gives an element $f \in F$ such that
\begin{align*}
\operatorname{acl}(P \cup F)
=
\operatorname{acl}(P \cup (F \setminus \{f\}) \cup \{e\})
\end{align*}
and $(F \setminus \{f\}) \cup \{e\}$ is independent over $P$. The latter condition implies that $F \setminus \{f\}$ is independent over $P \cup \{e\}$. Also $E_0$ is independent over $P \cup \{e\}$, because $E$ is independent over $P$. Moreover,
\begin{align*}
E_0 \subseteq \operatorname{acl}(P \cup F)
=
\operatorname{acl}(P \cup \{e\} \cup (F \setminus \{f\})).
\end{align*}
The induction hypothesis over $P \cup \{e\}$ gives
\begin{align*}
|E|-1 = |E_0| \leq |F \setminus \{f\}| = |F|-1.
\end{align*}
Hence $|E| \leq |F|$.
[/proof]
[guided]
The point of this step is to isolate the finite-dimensional part of the argument. Algebraic closure in a strongly minimal theory behaves like linear span in a [vector space](/page/Vector%20Space): the exchange axiom is the replacement rule, and the statement says that an independent set contained in the closure of $n$ independent elements cannot have more than $n$ elements.
We first prove the replacement move carefully, because this is the place where exchange must be used with the correct hypotheses. Let $P \subseteq M$ be a parameter set, let $X=\{x_1,\dots,x_m\} \subseteq M$ be finite and independent over $P$, and let $y \in \operatorname{acl}(P \cup X) \setminus \operatorname{acl}(P)$. Since $X$ is finite, choose the least $r \in \{1,\dots,m\}$ such that
\begin{align*}
y \in \operatorname{acl}(P \cup \{x_1,\dots,x_r\}).
\end{align*}
The minimality of $r$ gives
\begin{align*}
y \notin \operatorname{acl}(P \cup \{x_1,\dots,x_{r-1}\}).
\end{align*}
Now the [exchange axiom for algebraic closure in a strongly minimal theory](/page/Pregeometry) applies over the parameter set $P \cup \{x_1,\dots,x_{r-1}\}$ to the two elements $y$ and $x_r$. It gives
\begin{align*}
x_r \in \operatorname{acl}(P \cup \{x_1,\dots,x_{r-1}\} \cup \{y\})
\subseteq
\operatorname{acl}(P \cup (X \setminus \{x_r\}) \cup \{y\}).
\end{align*}
Because $y \in \operatorname{acl}(P \cup X)$ as well, monotonicity and idempotence imply the closure equality
\begin{align*}
\operatorname{acl}(P \cup X)
=
\operatorname{acl}(P \cup (X \setminus \{x_r\}) \cup \{y\}).
\end{align*}
We also need the replacement set to be independent. If $(X \setminus \{x_r\}) \cup \{y\}$ were dependent over $P$, then, since $X \setminus \{x_r\}$ is already independent over $P$, the dependence must involve $y$. There are two possible forms. First, the dependence may be witnessed directly by $y$: for some finite $H \subseteq X \setminus \{x_r\}$,
\begin{align*}
y \in \operatorname{acl}(P \cup H).
\end{align*}
Second, the dependence may initially be witnessed by an element $z \in X \setminus \{x_r\}$. Then for some finite $H \subseteq X \setminus \{x_r,z\}$,
\begin{align*}
z \in \operatorname{acl}(P \cup H \cup \{y\}).
\end{align*}
Because $X$ is independent over $P$, the element $z$ is not in $\operatorname{acl}(P \cup H)$. Therefore the exchange axiom applies over the parameter set $P \cup H$ to $z$ and $y$, and gives
\begin{align*}
y \in \operatorname{acl}(P \cup H \cup \{z\}) \subseteq \operatorname{acl}(P \cup (X \setminus \{x_r\})).
\end{align*}
Thus in either form of dependence, we obtain $y \in \operatorname{acl}(P \cup (X \setminus \{x_r\}))$. Substituting this into the relation placing $x_r$ in the closure of the previous elements and $y$ gives
\begin{align*}
x_r \in \operatorname{acl}(P \cup (X \setminus \{x_r\})),
\end{align*}
by monotonicity and idempotence. This contradicts the independence of $X$ over $P$. Hence $(X \setminus \{x_r\}) \cup \{y\}$ is independent over $P$.
Now let $E,F \subseteq M$ be finite, assume both are independent over $P$, and assume
\begin{align*}
E \subseteq \operatorname{acl}(P \cup F).
\end{align*}
We prove $|E| \leq |F|$ by induction on $|E|$, uniformly in the parameter set $P$. The uniform formulation is needed because after replacing one element of $F$ by one element of $E$, the induction is applied over the enlarged parameter set $P \cup \{e\}$.
If $E=\varnothing$, then $|E|=0 \leq |F|$. Assume $E$ is nonempty. Choose $e \in E$ and define
\begin{align*}
E_0 := E \setminus \{e\}.
\end{align*}
Since $E$ is independent over $P$, we have $e \notin \operatorname{acl}(P)$. Since $E \subseteq \operatorname{acl}(P \cup F)$, we have $e \in \operatorname{acl}(P \cup F)$. Applying the replacement lemma to $X=F$ and $y=e$ gives an element $f \in F$ such that
\begin{align*}
\operatorname{acl}(P \cup F)
=
\operatorname{acl}(P \cup (F \setminus \{f\}) \cup \{e\})
\end{align*}
and $(F \setminus \{f\}) \cup \{e\}$ is independent over $P$. This independence exactly says that $F \setminus \{f\}$ remains independent after $e$ is moved into the parameter set, that is, $F \setminus \{f\}$ is independent over $P \cup \{e\}$.
The set $E_0$ is independent over $P \cup \{e\}$ because $E$ was independent over $P$. The closure equality gives
\begin{align*}
E_0 \subseteq \operatorname{acl}(P \cup F)
=
\operatorname{acl}(P \cup \{e\} \cup (F \setminus \{f\})).
\end{align*}
Therefore the induction hypothesis applies over $P \cup \{e\}$ to $E_0$ and $F \setminus \{f\}$, yielding
\begin{align*}
|E|-1 = |E_0| \leq |F \setminus \{f\}| = |F|-1.
\end{align*}
Adding $1$ to both sides gives $|E| \leq |F|$.
[/guided]
[/step]
[step:Compare finite bases by applying the finite Steinitz bound in both directions]
Let $B,C \subseteq M$ be bases of $M$ over $A$, and suppose first that $B$ is finite. Since $C \subseteq M$ and $B$ spans $M$ over $A$,
\begin{align*}
C \subseteq \operatorname{acl}(A \cup B).
\end{align*}
For every finite set $E \subseteq C$, the set $E$ is independent over $A$ and satisfies $E \subseteq \operatorname{acl}(A \cup B)$. The finite Steinitz bound applied to this finite $E$ and to $F=B$ gives
\begin{align*}
|E| \leq |B|.
\end{align*}
Hence $C$ has no finite subset of cardinality $|B|+1$, so $C$ is finite and $|C| \leq |B|$. Reversing the roles of $B$ and $C$ gives $|B| \leq |C|$. Therefore $|B|=|C|$ when one of the two bases is finite.
[/step]
[step:Bound an infinite basis by finite supports in the other basis]
Assume now that $B$ is infinite. For every $c \in C$, the spanning property of $B$ gives
\begin{align*}
c \in \operatorname{acl}(A \cup B).
\end{align*}
By finite character of algebraic closure, there exists a finite set $F_c \subseteq B$ such that
\begin{align*}
c \in \operatorname{acl}(A \cup F_c).
\end{align*}
For each finite set $F \subseteq B$, define
\begin{align*}
C_F := C \cap \operatorname{acl}(A \cup F).
\end{align*}
The set $C_F$ is independent over $A$ because it is a subset of $C$, and it is contained in $\operatorname{acl}(A \cup F)$. For every finite set $E \subseteq C_F$, the finite Steinitz bound applied to $E$ and $F$ gives
\begin{align*}
|E| \leq |F|.
\end{align*}
Therefore $C_F$ has no finite subset of cardinality $|F|+1$, so $C_F$ is finite and $|C_F| \leq |F|$.
Since each $c \in C$ belongs to $C_{F_c}$, we have
\begin{align*}
C = \bigcup_{\substack{F \subseteq B\\ F \text{ finite}}} C_F.
\end{align*}
Because $B$ is infinite, the set of finite subsets of $B$ has cardinality $|B|$, and each $C_F$ is finite. Therefore
\begin{align*}
|C| \leq |B|.
\end{align*}
[/step]
[step:Reverse the comparison to obtain equality of dimensions]
If $C$ is finite, then the finite case already gives $|B|=|C|$. Otherwise $C$ is infinite, and the preceding argument with the names of $B$ and $C$ interchanged gives
\begin{align*}
|B| \leq |C|.
\end{align*}
Together with the inequality $|C| \leq |B|$ obtained above, the [Cantor--Schroeder--Bernstein theorem](/page/Cantor-Schroeder-Bernstein%20Theorem) gives
\begin{align*}
|B| = |C|.
\end{align*}
Thus any two bases of $M$ over $A$ have the same cardinality, and the theorem is proved.
[/step]
