Vector space/Basis/Exchange lemma/Fact

Basis exchange lemma

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

where for some fixed .

Then also the family
is a basis of .