theorem :: ZMODUL01:26

for V being Z_Module
for W being Submodule of V holds 0. W = 0. V by VECTSP_4:def 2;