Vector space/Basis/Exchange theorem/Fact

Let ${\displaystyle {}K}$ denote a field, let ${\displaystyle {}V}$ denote a ${\displaystyle {}K}$-vector space, and let a basis ${\displaystyle {}b_{1},\ldots ,b_{n}}$ of ${\displaystyle {}V}$ be given. Let

${\displaystyle u_{1},\ldots ,u_{k}}$

denote a family of linearly independent vectors in ${\displaystyle {}V}$.

Then there exists a subset

${\displaystyle {}J=\{i_{1},i_{2},\ldots ,i_{k}\}\subseteq \{1,\ldots ,n\}=I\,}$

such that the family

${\displaystyle u_{1},\ldots ,u_{k},b_{i},i\in I\setminus J,}$

is a basis of ${\displaystyle {}V}$.

In particular, ${\displaystyle {}k\leq n}$.