The Steinitz Exchange Lemma

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$.

(i) Independent families are no longer than spanning families. Let $m,n\in\mathbb{N}_{0}$, let $(u_{1},\dots,u_{m})$ be a linearly independent $m$-tuple in $V$, and let $(w_{1},\dots,w_{n})$ be an $n$-tuple in $V$ that spans $V$. Then $m\leq n$.