theorem :: ZMODUL01:87

for R being Ring
for V being LeftMod of R
for u being Vector of V
for W being Submodule of V
for C being Coset of W holds
( u in C iff C = u + W ) by VECTSP_4:77;