Vector space/Basis/Exchange theorem/Fact

Basis exchange theorem

Let $K$ denote a field, let $V$ denote a $K$-vector space, and let a basis $b_1,\dots ,b_n$ of $V$ be given. Let

$u_1,\dots ,u_k$

denote a family of linearly independent vectors in $V$.

Then there exists a subset

$J=\{i_1,i_2,\dots ,i_k\}\subseteq \{1,\dots ,n\}=I$

such that the family

$u_1,\dots ,u_k,b_i,i\in I\setminus J,$

is a basis of $V$.

In particular, $k\le n$.

Proof, Write another proof