let O be set ; :: thesis: for G, H, I being GroupWithOperators of O
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I
let G, H, I be GroupWithOperators of O; :: 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 o being Element of O
for g being Element of G holds f . ((G ^ o) . g) = (I ^ o) . (f . g)

let o be Element of O; :: thesis: for g being Element of G holds f . ((G ^ o) . g) = (I ^ o) . (f . g)
let g be Element of G; :: thesis: f . ((G ^ o) . g) = (I ^ o) . (f . g)
thus f . ((G ^ o) . g) = h1 . (h . ((G ^ o) . g)) by FUNCT_2:15
.= h1 . ((H ^ o) . (h . g)) by Def18
.= (I ^ o) . (h1 . (h . g)) by Def18
.= (I ^ o) . (f . g) by FUNCT_2:15 ; :: thesis: verum

end;

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