{} 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_{1} being Subset of V st

( b_{1} is linearly-independent & Lin b_{1} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
; :: thesis: verum

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

( b