let G, H, I be AddGroup; :: thesis: for h being Homomorphism of G,H

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h1 be Homomorphism of H,I; :: thesis: h1 * h is Homomorphism of G,I

reconsider f = h1 * h as Function of G,I ;

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h1 be Homomorphism of H,I; :: thesis: h1 * h is Homomorphism of G,I

reconsider f = h1 * h as Function of G,I ;

now :: thesis: for a, b being Element of G holds f . (a + b) = (f . a) + (f . b)

hence
h1 * h is Homomorphism of G,I
by VECTSP_1:def 20; :: thesis: verumlet a, b be Element of G; :: thesis: f . (a + b) = (f . a) + (f . b)

thus f . (a + b) = h1 . (h . (a + b)) by FUNCT_2:15

.= h1 . ((h . a) + (h . b)) by VECTSP_1:def 20

.= (h1 . (h . a)) + (h1 . (h . b)) by VECTSP_1:def 20

.= (f . a) + (h1 . (h . b)) by FUNCT_2:15

.= (f . a) + (f . b) by FUNCT_2:15 ; :: thesis: verum

end;thus f . (a + b) = h1 . (h . (a + b)) by FUNCT_2:15

.= h1 . ((h . a) + (h . b)) by VECTSP_1:def 20

.= (h1 . (h . a)) + (h1 . (h . b)) by VECTSP_1:def 20

.= (f . a) + (h1 . (h . b)) by FUNCT_2:15

.= (f . a) + (f . b) by FUNCT_2:15 ; :: thesis: verum