theorem :: ZMODUL01:27
for V being Z_Module
for W1, W2 being Submodule of V holds 0. W1 = 0. W2 by VECTSP_4:12;