theorem Th11: :: RMOD_3:11

for R being Ring
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 #) )