let V be RealLinearSpace; 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; ( ( 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
; 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; verum