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
consider W' being strict Subspace of M such that
A1: the carrier of ((Omega). M) = the carrier of W' ;
thus M in Subspaces M by A1, Def3; :: thesis: verum