for R being Ring
for V being LeftMod 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 by VECTSP_4:81;