theorem :: RMOD_2:71

for R being Ring
for V being RightMod of R holds the carrier of V is Coset of (Omega). V