let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V holds W is Submodule of (Omega). V
let V be RightMod of R; :: thesis: for W being Submodule of V holds W is Submodule of (Omega). V
let W be Submodule of V; :: thesis: W is Submodule of (Omega). V
thus the carrier of W c= the carrier of ((Omega). V) by RMOD_2:def 2; :: according to RMOD_2:def 2 :: thesis: ( 0. W = 0. ((Omega). V) & the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] )
thus 0. W = 0. V by RMOD_2:def 2
.= 0. ((Omega). V) ; :: thesis: ( the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] )
thus ( the U7 of W = the U7 of ((Omega). V) | [: the carrier of W, the carrier of W:] & the rmult of W = the rmult of ((Omega). V) | [: the carrier of W, the carrier of R:] ) by RMOD_2:def 2; :: thesis: verum