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:15
.= 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:15
.= 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