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

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