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 VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W being Subspace of M holds W is Subspace of (Omega). M
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W being Subspace of M holds W is Subspace of (Omega). M
let W be Subspace of M; :: thesis: W is Subspace of (Omega). M
thus the carrier of W c= the carrier of ((Omega). M) by VECTSP_4:def 2; :: according to VECTSP_4:def 2 :: thesis: ( 0. W = 0. ((Omega). M) & the U7 of W = K97(the U7 of ((Omega). M),the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [:the carrier of GF,the carrier of W:] )
thus 0. W = 0. M by VECTSP_4:def 2
.= 0. ((Omega). M) by VECTSP_4:def 2 ; :: thesis: ( the U7 of W = K97(the U7 of ((Omega). M),the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [:the carrier of GF,the carrier of W:] )
thus ( the U7 of W = K97(the U7 of ((Omega). M),the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [:the carrier of GF,the carrier of W:] ) by VECTSP_4:def 2; :: thesis: verum