theorem :: ZMODUL01:75

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