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

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