let U1, U2, U3 be Universal_Algebra; :: thesis: for h being Function of U1,U2
for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
let h be Function of U1,U2; :: thesis: for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
let h1 be Function of U2,U3; :: thesis: ( h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 implies h1 * h is_isomorphism U1,U3 )
assume A1: ( h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 ) ; :: thesis: h1 * h is_isomorphism U1,U3
then A2: ( h is one-to-one & h1 is one-to-one ) by Th8;
A3: rng (h1 * h) = the carrier of U3

proof

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

end;

A5: h1 * h is one-to-one by A2;
( h is_homomorphism U1,U2 & h1 is_homomorphism U2,U3 ) by A1, Th8;
then h1 * h is_homomorphism U1,U3 by Th7;
hence h1 * h is_isomorphism U1,U3 by A3, A5, Th8; :: thesis: verum