{} the carrier of V is linearly-independent by Th7;
then ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by Th24;
hence ex b₁ being Subset of V st
( b₁ is linearly-independent & Lin b₁ = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) ; :: thesis: verum