theorem :: ZMODUL01:73

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