set B = the Basis of (VecSp (E,F));
set v = the Element of the Basis of (VecSp (E,F));
the Element of the Basis of (VecSp (E,F)) in the Basis of (VecSp (E,F)) ;
then { the Element of the Basis of (VecSp (E,F))} c= the Basis of (VecSp (E,F)) by TARSKI:def 1;
hence ex b₁ being Subset of (VecSp (E,F)) st
( not b₁ is empty & b₁ is finite & b₁ is linearly-independent ) by VECTSP_7:1; :: thesis: verum