Vector space/Basis/Exchange lemma/Fact
              < Vector space < Basis < Exchange lemma 
 
            
          
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