Is the Steinitz exchange lemma necessary to establish invariance of 'basis-size'? I am going to answer my own question in some sense...
In Beardon's "Algebra and Geometry" he proves (Theorem 7.2.2) that if $v_1,\ldots,v_n$ and $u_1,\ldots,u_m$ are both bases for some $F$-vector space $V$, then $n=m$. He does so relying (essentially) only on commutativity in $F$. 
This seems strange as almost all other books on the subject stress the importance of the Steinitz Exchange Lemma in establishing the notion of dimension. So my question this: Why do they all bother with/make a fuss about Steinitz Exchange?
Many thanks!

Here is a sketch of Beardon's proof:
Write $u_1$ in terms of the $v_j$ and write each $v_j$ in terms of the $u_i$.  Then by equating coefficients we obtain something like $1=\sum_{j=1}^n\lambda_{jk}\mu_{kj}$ for each $k=1,\ldots,m$ so by summing over $k$ we obtain $$m=\sum_{k=1}^m\sum_{j=1}^n\lambda_{jk}\mu_{kj}.$$ But by symmetry we also have $$n=\sum_{k=1}^n\sum_{j=1}^m\lambda_{jk}\mu_{kj}.$$ The result follows.
 A: As mentioned in the comments, Beardon's proof only works if the characteristic of the underlying ring is zero.
A: In fact, you can introduce finite dimensional vector spaces over any field without any reference to Steinitz, Gauss or other matrix operations (solution of equations or inversion) using the following lemma:
Every $n$-sequence of linearly independent vectors (frame for short)  $\|e_j\|_n$ is maximal in its linear span $[\|e_j\|_n]$ (no longer sequence of linearly independent vectors exists there).
From this lemma, one can easily define the basis and dimension of a linear space as well as Steinitz's lemma and many other important facts.
The equivalent formulation is:
For every $n$-sequence of linearly independent vectors $\|f_j\|_n\in[\|e_j\|_n]$, the following system of inclusions hold:
$e_i\in[\|f_j\|_n], \ i=1,\ldots,n$
It can be proved only using special linear mappings and its kernel.
That means that you do not need Steinitz, Gauss and co. at the very beginning. You do not even need to know matrix manipulations and the solution of linear equations.
The only thing you need are the axioms, definiton of linear mappings and the notion of the kernel. 
The proof is by induction performed on the rank $n$ of the frame $\|e_j\|_n$. The assertion is evident for $n=1$ since in this case the linear span coincides with the family of vectors
$$
[\|e_j\|_1]=\left\{\lambda e_1|\, \lambda\in\Lambda\right\}.
$$
Assuming that the assertion is proved for all natural $k\le n-1$, consider the case $k=n$. Introduce $n$ linear mappings
$$
L_i\in Hom\left([\|e_j\|_n], [\|f_1,\ldots,\hat f_i,\ldots,f_n\|]\right),\quad i=1,\ldots,n,
$$
by defining $L_i$ on vectors $e_1,\ldots,e_n$ according to the equations
$$
L_ie_j=f_j,\ i\neq j,\ \ L_ie_i=0,\quad i,j=1,\ldots,n.
$$
The kernel of $L_i$ coincides with the subspace
$$
ker L_i=\{\lambda e_i\bigr|\lambda\in\Lambda\},
$$
and the image  ---  with the linear span
$$
 im\,L_i=[\|f_1,\ldots,\hat f_i,\ldots f_n\|].
$$
The restriction of $L_i$ on the subspace $[\|f_j\|_n]\subset [\|e_j\|_n]$ has a nonzero kernel since otherwise the $n$-frame $\|L_if_j\|, j=1,\ldots,n$ would be embedded in the linear span of an $(n-1)$-frame $\|f_1,\ldots,\hat f_i,\ldots,f_n\|$, which contradicts the inductive assumption. Hence,
$$
\lambda e_i\in ker L_i\Bigr|_{[\|f_j\|_n]} \  \forall\lambda\in\Lambda,\ i=1,\ldots,n,
$$
or
$$
e_i\in[\|f_j\|_n]\ \forall i=1,\ldots,n.
$$
