theorem :: ZMODUL01:90

for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W ) by VECTSP_4:80;