let H, G, I be Group; :: 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

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:21
.= h1 . ((h . a) * (h . b)) by Def7
.= (h1 . (h . a)) * (h1 . (h . b)) by Def7
.= (f . a) * (h1 . (h . b)) by FUNCT_2:21
.= (f . a) * (f . b) by FUNCT_2:21 ; :: thesis: verum

end;

hence h1 * h is Homomorphism of G,I by Def7; :: thesis: verum