Solution (source code)

= Solution

Let $u_1,\ldots,u_m$ and $v_1,\ldots,v_n$ be two finite <bases> of the <vector space> $V$. We prove the underlying exchange argument rather than assuming that <dimension> is already well-defined.

More generally, suppose $u_1,\ldots,u_m$ are <linearly independent> and $v_1,\ldots,v_n$ form a <spanning set>. Starting with the spanning list of $v$'s, replace one of its members by $u_1$. Indeed, express $u_1$ as a linear combination of that list; at least one coefficient is nonzero, so we can solve for its corresponding $v_j$ and retain a spanning list. Inductively, suppose the spanning list now consists of $u_1,\ldots,u_r$ and $n-r$ of the original $v$'s. Express $u_{r+1}$ in that list. Some coefficient of a remaining $v$ must be nonzero, since otherwise $u_{r+1}$ would lie in the span of the preceding $u$'s, contradicting <linear independence>. Solve for that $v$ and replace it by $u_{r+1}$.

If $m>n$, after $n$ replacements the spanning list consists of $u_1,\ldots,u_n$, forcing $u_{n+1}$ to lie in their span, again a contradiction. Thus every finite <linearly independent> list has at most as many members as every finite <spanning set>. This proves the <Steinitz exchange lemma> in the form required here. Applying it to the two <bases> in both orders gives $m\leq n$ and $n\leq m$, hence \b[$m=n$]. The zero <vector space> has only the empty <basis>, which also fits the argument.