theorem Th7: :: LMOD_XX1:7

for M being AbGroup
for f being Element of set_End M holds (ADD (M,M)) . (f,(Inv f)) = ZeroMap (M,M)