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 ;

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

let 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;

hence h1 * h is Homomorphism of G,I by VECTSP_1:def 20; :: thesis: verum