:: deftheorem Def6 defines Coset RMOD_2:def 6 :
for R being Ring
for V being RightMod of R
for W being Submodule of V
for b₄ being Subset of V holds
( b₄ is Coset of W iff ex v being Vector of V st b₄ = v + W );