let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable strict VectSp-like Abelian add-associative right_zeroed VectSpStr of GF holds M in Subspaces M
let M be non empty right_complementable strict VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: M in Subspaces M
ex W' being strict Subspace of M st the carrier of ((Omega). M) = the carrier of W' ;
hence M in Subspaces M by Def3; :: thesis: verum