theorem :: ZMODUL01:74

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 v being Vector of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W ) by VECTSP_4:63;