for R being Ring
for V being strict RightMod of R holds
( ((0). V) + ((Omega). V) = V & ((Omega). V) + ((0). V) = V ) by Th9;