theorem :: ZMODUL01:89

for R being Ring
for V being LeftMod of R
for u, v being Vector of V
for W being Submodule of V
for C being Coset of W st u in C & v in C holds
ex v1 being Vector of V st
( v1 in W & u - v1 = v ) by VECTSP_4:79;