theorem :: ZMODUL01:93

for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V
for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2 by VECTSP_5:2;