[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$.[/step]

[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: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][/step]

[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: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]