theorem :: RMOD_3:12
for R being Ring
for V being strict RightMod of R holds ((Omega). V) + ((Omega). V) = V by Th11;