let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V holds
( ((Omega). V) + W = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) )
let V be RightMod of R; :: thesis: for W being Submodule of V holds
( ((Omega). V) + W = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) )
let W be Submodule of V; :: thesis: ( ((Omega). V) + W = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) )
consider W' being strict Submodule of V such that
A1: the carrier of W' = the carrier of ((Omega). V) ;
A2: the carrier of W c= the carrier of W' by A1, RMOD_2:def 2;
A3: W' is Submodule of (Omega). V by Lm5;
W + ((Omega). V) = W + W' by A1, Lm4
.= W' by A2, Lm3
.= RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) by A1, A3, RMOD_2:39 ;
hence ( ((Omega). V) + W = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V,the U7 of V,the U2 of V,the rmult of V #) ) by Lm1; :: thesis: verum