let R be comRing; :: thesis: for M being LeftMod of R
for a being Element of R holds (canHom M) . a is Homomorphism of (AbGr M),(AbGr M)
let M be LeftMod of R; :: thesis: for a being Element of R holds (canHom M) . a is Homomorphism of (AbGr M),(AbGr M)
let a be Element of R; :: thesis: (canHom M) . a is Homomorphism of (AbGr M),(AbGr M)
(canHom M) . a in set_End (AbGr M) ;
then consider f being Function of the carrier of (AbGr M), the carrier of (AbGr M) such that
A1: ( f = (canHom M) . a & f is Endomorphism of (AbGr M) ) ;
thus (canHom M) . a is Homomorphism of (AbGr M),(AbGr M) by A1; :: thesis: verum