let R be comRing; :: thesis: for M, N being LeftMod of R
for f being Homomorphism of R,M,N holds AbGr f is Homomorphism of (AbGr M),(AbGr N)
let M, N be LeftMod of R; :: thesis: for f being Homomorphism of R,M,N holds AbGr f is Homomorphism of (AbGr M),(AbGr N)
let f be Homomorphism of R,M,N; :: thesis: AbGr f is Homomorphism of (AbGr M),(AbGr N)
for x, y being Element of (AbGr M) holds (AbGr f) . (x + y) = ((AbGr f) . x) + ((AbGr f) . y)

proof

let x, y be Element of (AbGr M); :: thesis: (AbGr f) . (x + y) = ((AbGr f) . x) + ((AbGr f) . y)
reconsider x1 = x, y1 = y as Element of the carrier of M ;
A2: (AbGr f) . x = f . x1 by Def26;
A4: (AbGr f) . y = f . y1 by Def26;
reconsider z1 = x + y as Element of the carrier of M ;
A6: (AbGr f) . z1 = f . z1 by Def26;
A7: z1 = x1 + y1 ;
(AbGr f) . (x + y) = (f . x1) + (f . y1) by A6, A7, Def10, VECTSP_1:def 20
.= ((AbGr f) . x) + ((AbGr f) . y) by A2, A4 ;
hence (AbGr f) . (x + y) = ((AbGr f) . x) + ((AbGr f) . y) ; :: thesis: verum

end;

hence AbGr f is Homomorphism of (AbGr M),(AbGr N) by VECTSP_1:def 20; :: thesis: verum