:: deftheorem defines 0_End LMOD_XX1:def 6 :
for M being AbGroup holds 0_End M = ZeroMap (M,M);