let G, H, I be Group; :: thesis: for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: G,H) = 1: G,I & (1: H,I) * h = 1: G,I )
let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds
( h1 * (1: G,H) = 1: G,I & (1: H,I) * h = 1: G,I )
let h1 be Homomorphism of H,I; :: thesis: ( h1 * (1: G,H) = 1: G,I & (1: H,I) * h = 1: G,I )

A1: now

let a be Element of G; :: thesis: ((1: H,I) * h) . a = 1_ I
thus ((1: H,I) * h) . a = (1: H,I) . (h . a) by FUNCT_2:21
.= 1_ I by Def8 ; :: thesis: verum

end;

now

let a be Element of G; :: thesis: (h1 * (1: G,H)) . a = 1_ I
thus (h1 * (1: G,H)) . a = h1 . ((1: G,H) . a) by FUNCT_2:21
.= h1 . (1_ H) by Def8
.= 1_ I by Th40 ; :: thesis: verum

end;

hence ( h1 * (1: G,H) = 1: G,I & (1: H,I) * h = 1: G,I ) by A1, Def8; :: thesis: verum