let G, H, I be Group; :: thesis: for h being Homomorphism of G,H
for h1 being Homomorphism of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h1 be Homomorphism of H,I; :: thesis: ( h is bijective & h1 is bijective implies h1 * h is bijective )
assume A1: ( h is bijective & h1 is bijective ) ; :: thesis: h1 * h is bijective
then A2: ( h is one-to-one & h1 is one-to-one ) ;
A3: rng (h1 * h) = the carrier of I

proof

A4: dom h1 = the carrier of H by FUNCT_2:def 1;
rng h = the carrier of H by A1, Th70;
hence rng (h1 * h) = rng h1 by A4, RELAT_1:47
.= the carrier of I by A1, Th70 ;
:: thesis: verum

end;

h1 * h is one-to-one by A2;
hence h1 * h is bijective by A3, Th70; :: thesis: verum