theorem :: ZMODUL01:150
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for v being Vector of V ex C being Coset of W st v in C by Lm18;