:: deftheorem Def27 defines canHom LMOD_XX1:def 27 :
for R being comRing
for M being LeftMod of R
for b₃ being Function of R,(End_Ring (AbGr M)) holds
( b₃ = canHom M iff for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & b₃ . x = AbGr f ) );