Proof of Existence and Invariance of the Length of a Basis

If an $n$-tuple $(v_{1},\dots,v_{n})$ spans $V$, then A Finite Spanning Family Contains a Basis (i) gives $m\leq n$ and a strictly increasing map $k:[m]\to[n]$ such that the $m$-tuple $(v_{k(1)},\dots,v_{k(m)})$ is a basis of $V$. This proves (i).

Now let $(b_{1},\dots,b_{m})$ and $(c_{1},\dots,c_{n})$ be bases of $V$. By Finite Basis of a Vector Space (i) the first is linearly independent and the second spans $V$, so $m\leq n$ by The Steinitz Exchange Lemma (i). Exchanging the roles of the two bases gives $n\leq m$. Hence $m=n$, which proves (ii).