let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds V is Subspace of (Omega). V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: V is Subspace of (Omega). V
reconsider VS = V as Subspace of V by Th24;
for v being Vector of V st v in VS holds
v in (Omega). V ;
hence V is Subspace of (Omega). V by Th28; :: thesis: verum