theorem Th99: :: ZMODUL01:99

for V being Z_Module
for W being strict Submodule of V holds ((0). V) + W = W by VECTSP_5:9;