Subgroups of free abelian groups are free

Well-order $B$. For $b\in B$, let $F_{\le b}$ be the span of the $e_c$ with $c\le b$, and put $H_{\le b}=H\cap F_{\le b}$. The $b$-coordinate homomorphism ${\pi }_b:F_{\le b}\to \mathbb{Z}$ has image ${\pi }_b(H_{\le b})=d_b\mathbb{Z}$ for a uniquely determined $d_b\ge 0$. Put $D=\{b\in B:d_b>0\}$.

For each $b\in D$ the set $X_b=\{x\in H_{\le b}:{\pi }_b(x)=d_b\}$ is nonempty. Apply AC to this set-indexed family and fix $x_b\in X_b$ simultaneously for all $b\in D$. These are the only choices of lifts in the argument; they do not depend recursively on previously chosen bases.

We prove by well-ordered induction on $b$ that $H_{\le b}$ is spanned by $x_c$ with $c\in D$ and $c\le b$. Suppose this is proved below $b$, and take $h\in H_{\le b}$. If $d_b>0$, write ${\pi }_b(h)=q{d}_b$ and set $h^{\mathrm{\prime }}=h-q{x}_b$; if $d_b=0$, set $h^{\mathrm{\prime }}=h$. In both cases $h^{\mathrm{\prime }}\in H$ has finite support strictly below $b$. If that support is empty, $h^{\mathrm{\prime }}=0$. Otherwise it has a greatest element $c<b$, and $h^{\mathrm{\prime }}\in H_{\le c}$ is in the required span by the induction hypothesis. Thus so is $h$. Conversely all the indicated $x_c$ belong to $H_{\le b}$. This verifies the inductive implication, including the least-element and limit cases, and [L4] proves the assertion for every $b$.

The family $(x_b{)}_{b\in D}$ is linearly independent. Indeed, in a nonzero finite relation choose the greatest index $b$ with nonzero coefficient $n_b$. Its $b$-coordinate is $n_b{d}_b$, since all smaller-indexed vectors have zero $b$-coordinate. This is nonzero in $\mathbb{Z}$, contradicting the relation. Every nonzero $h\in H$ has a greatest basis-support index $b$ and belongs to $H_{\le b}$, so step 3.1 also proves spanning of all $H$. Hence $(x_b{)}_{b\in D}$ is a basis. If $B$ or $D$ is empty the same reasoning says $H=0$ with empty basis.