theorem :: RMOD_2:73

for R being Ring
for V being RightMod of R
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )