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:1;
hence W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:31; :: thesis: verum