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 ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF 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 ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF 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 ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) )
consider W9 being strict Submodule of V such that
A1: the carrier of W9 = the carrier of ((Omega). V) ;
A2: the carrier of W c= the carrier of W9 by A1, RMOD_2:def 2;
A3: W9 is Submodule of (Omega). V by Lm5;
W + ((Omega). V) = W + W9 by A1, Lm4
.= W9 by A2, Lm3
.= RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) by A1, A3, RMOD_2:31 ;
hence ( ((Omega). V) + W = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) & W + ((Omega). V) = RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) ) by Lm1; :: thesis: verum