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 strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds M in Subspaces M
let M be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: M in Subspaces M
ex W9 being strict Subspace of M st the carrier of ((Omega). M) = the carrier of W9 ;
hence M in Subspaces M by Def3; :: thesis: verum