Vector space/Basis/Exchange theorem/Fact

Basis exchange theorem

Let denote a field, let denote a -vector space, and let a basis of be given. Let

denote a family of linearly independent vectors in .

Then there exists a subset

such that the family

is a basis of .

In particular, .