let R be comRing; :: thesis: for M being LeftMod of R holds canHom M is multiplicative
let M be LeftMod of R; :: thesis: canHom M is multiplicative
for x, y being Element of R holds (canHom M) . (x * y) = ((canHom M) . x) * ((canHom M) . y)

proof

let x, y be Element of R; :: thesis: (canHom M) . (x * y) = ((canHom M) . x) * ((canHom M) . y)
consider f being Endomorphism of R,M such that
A1: ( f = (curry the lmult of M) . x & (canHom M) . x = AbGr f ) by Def27;
consider g being Endomorphism of R,M such that
A2: ( g = (curry the lmult of M) . y & (canHom M) . y = AbGr g ) by Def27;
consider h being Endomorphism of R,M such that
A3: ( h = (curry the lmult of M) . (x * y) & (canHom M) . (x * y) = AbGr h ) by Def27;
reconsider f0 = f, g0 = g, h0 = h as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8;
A4: for m being Element of M holds h . m = (f * g) . m

proof

let m be Element of M; :: thesis: h . m = (f * g) . m
A5: g . m = y * m by A2, LOPBAN_8:7;
reconsider ym = y * m as Element of the carrier of M ;
h0 . m = (x * y) * m by A3, LOPBAN_8:7
.= x * ym by VECTSP_1:def 16
.= f0 . (g0 . m) by A5, A1, LOPBAN_8:7
.= (f0 * g0) . m by FUNCT_2:15 ;
hence h . m = (f * g) . m ; :: thesis: verum

end;

reconsider f1 = AbGr f, g1 = AbGr g as Endomorphism of (AbGr M) by Th28;
h = f * g by A4;
then (canHom M) . (x * y) = (FuncComp (AbGr M)) . (f1,g1) by A3, Th34
.= ((canHom M) . x) * ((canHom M) . y) by A1, A2, Th6 ;
hence (canHom M) . (x * y) = ((canHom M) . x) * ((canHom M) . y) ; :: thesis: verum

end;

hence canHom M is multiplicative by GROUP_6:def 6; :: thesis: verum