:: deftheorem defines mult_End LMOD_XX1:def 5 :
for M being AbGroup holds mult_End M = (FuncComp M) | [:(set_End M),(set_End M):];