let V be RealLinearSpace; :: thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #)
let W be strict Subspace of V; :: thesis: ( ( for v being VECTOR of V holds v in W ) implies W = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) )
assume for v being VECTOR of V holds v in W ; :: thesis: W = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #)
then for v being VECTOR of V holds
( v in W iff v in (Omega). V ) by RLVECT_1:3;
hence W = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) by RLSUB_1:39; :: thesis: verum