Existence and Invariance of the Length of a Basis

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $K$, with $+$, $\cdot$, $0$ and $1$, be a field, and let $V$, with its addition and scalar multiplication, be a vector space over $K$. Spanning families are as in Span of a Finite Family; Spanning Families (iii) and bases as in Finite Basis of a Vector Space (i).

(i) Existence of a basis. If $n\in\mathbb{N}_{0}$ and some $n$-tuple in $V$ spans $V$, then there are $m\in\mathbb{N}_{0}$ with $m\leq n$ and an $m$-tuple in $V$ that is a basis of $V$.

(ii) Invariance of the length. If $(b_{1},\dots,b_{m})$ and $(c_{1},\dots,c_{n})$ are bases of $V$, with $m,n\in\mathbb{N}_{0}$, then $m=n$.