for R being Ring
for V being RightMod of R
for v being Vector of V holds {v} is Coset of (0). V