let R be comRing; :: thesis: for M being LeftMod of R holds canHom M is additive
let M be LeftMod of R; :: thesis: canHom M is additive
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;
reconsider f1 = AbGr f, g1 = AbGr g as Endomorphism of (AbGr M) by Th28;
for m being Element of the carrier of M holds h . m = (f . m) + (g . m)

proof

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

end;

then A6: h0 = (ADD (M,M)) . (f0,g0) by Th15;
(canHom M) . (x + y) = (ADD ((AbGr M),(AbGr M))) . (f1,g1) by A3, A6, Th31
.= ((canHom M) . x) + ((canHom M) . y) by A1, A2, Th3 ;
hence (canHom M) . (x + y) = ((canHom M) . x) + ((canHom M) . y) ; :: thesis: verum

end;

hence canHom M is additive ; :: thesis: verum