for R being Ring
for V being RightMod of R
for u being Vector of V
for W being Submodule of V
for B, C being Coset of W st u in B & u in C holds
B = C