theorem HM0: :: ZMODUL06:41

for X, Y being Z_Module
for L being linear-transformation of X,Y holds L . (0. X) = 0. Y