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 that
A1: h is bijective and
A2: h1 is bijective ; :: thesis: h1 * h is bijective
( dom h1 = the carrier of H & rng h = the carrier of H ) by A1, Th70, FUNCT_2:def 1;
then rng (h1 * h) = rng h1 by RELAT_1:47
.= the carrier of I by A2, Th70 ;
hence h1 * h is bijective by A1, A2, Th70; :: thesis: verum