Any two bases of a free abelian group have the same cardinality. I am comfortable with understanding the theorem when the basis has a finite number of elements.
In the case where the basis is infinite, I find the proof very overwhelming and not so elegant. 
Can someone give an accessible proof for the infinite case? Or at least a rough sketch of ideas involved in proving it?
Update: I would be comfortable if some set theoretic approach is used(in particular Cardinal Numbers).
 A: The proof is easy provided you know the following facts about infinite sets:

  
*
  
*If $A$ is infinite then $|A| = |\mathcal{P}_{\mathrm{fin}}(A)|$, where 
  $\mathcal{P}_{\mathrm{fin}}(A)$ is the set of finite subsets of $A$
  
*If $f \colon A \to B$ is a map between infinite sets such that the fibers $f^{-1}(b)$ are finite for all $b \in B$ then $|A| \leq |B|$

Now suppose $B_1$ and $B_2$ are infinite bases of an abelian group $A$. Let $f \colon B_1 \to \mathcal{P}_{\mathrm{fin}}(B_2)$ be the map sending an element $b \in B_1$ to the smallest subset $U \subset B_2$ such that $b$ lies in the span of $U$. By the arguments mentioned above, it follows $|B_1| \leq |\mathcal{P}_{\mathrm{fin}}(B_2)| = |B_2|$. Of course, by symmetry, we also have $|B_2| \leq |B_1|$.
If I am not mistaken, this proof carries over verbatim for free modules of infinite rank over arbitrary rings.
A: Yes, nothing mysterious: The commutative free group with basis $X$ is just $\mathbb{Z}^{(X)}$, i.e. the (additive) group of all functions $X\to \mathbb{Z}$ with finite support (the support of $f:\,X\to\mathbb{Z}$ is the set $supp(f)=\{x\in X|f(x)\not=0\}$). 
Now allowing denominators, if $\mathbb{Z}^{(X)}\simeq \mathbb{Z}^{(Y)}$ we have 
$$
\mathbb{Q}^{(X)}=\mathbb{Q}\otimes_\mathbb{Z}\,\mathbb{Z}^{(X)}
\simeq
\mathbb{Q}\otimes_\mathbb{Z}\,\mathbb{Z}^{(Y)}=\mathbb{Q}^{(Y)}
$$
we are now in the realm of vector spaces and the two bases $X,\, Y$ are in bijection.
Remark: In noncommutative case, you have the same property 
$$
F(X)\simeq F(Y)\Longrightarrow |X|=|Y|
$$ 
(finite or infinite case). You can (a) use cardinality argument (infinite case only) (b) abelianize and remark that $F(X)^{ab}\simeq \mathbb{Z}^{(X)}$ (c) use Magnus transformation which I describe now. Magnus transformation is $\mu:\,x\mapsto 1+x$ sends $X\to\mathbb{Z}\langle\langle X\rangle\rangle$ (more precisely to $1+\mathbb{Z}_+\langle\langle X\rangle\rangle$ i.e. the group of series with constant term $1$). Then you get $\mathbb{Z}.X$ by quotients (or, which amounts to the same, considering the linear part of the series obtained).
