theorem LMThSumMod2: :: ZMODUL06:31

for V being Z_Module
for W being Submodule of V
for W1s, W2s being Submodule of W
for W1, W2 being Submodule of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2