let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W being Subspace of M holds W is Subspace of (Omega). M
let W be Subspace of M; :: thesis: W is Subspace of (Omega). M
thus the carrier of W c= the carrier of ((Omega). M) by VECTSP_4:def 2; :: according to VECTSP_4:def 2 :: thesis: ( 0. W = 0. ((Omega). M) & the addF of W = K116( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus 0. W = 0. M by VECTSP_4:def 2
.= 0. ((Omega). M) by VECTSP_4:def 2 ; :: thesis: ( the addF of W = K116( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus ( the addF of W = K116( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] ) by VECTSP_4:def 2; :: thesis: verum