{} the carrier of V is linearly-independent by RLVECT_3:8;
then ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V,the U2 of V,the U5 of V,the Mult of V,the scalar of V #) ) by Th11;
hence ex b₁ being Subset of V st
( b₁ is linearly-independent & Lin b₁ = UNITSTR(# the carrier of V,the U2 of V,the U5 of V,the Mult of V,the scalar of V #) ) ; :: thesis: verum