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 that
A1: h is_isomorphism U1,U2 and
A2: h1 is_isomorphism U2,U3 ; :: thesis: h1 * h is_isomorphism U1,U3
( dom h1 = the carrier of U2 & rng h = the carrier of U2 ) by A1, Th9, FUNCT_2:def 1;
then A3: rng (h1 * h) = rng h1 by RELAT_1:28
.= the carrier of U3 by A2, Th9 ;
( h is_homomorphism U1,U2 & h1 is_homomorphism U2,U3 ) by A1, A2, Th8;
then A4: h1 * h is_homomorphism U1,U3 by Th7;
( h is one-to-one & h1 is one-to-one ) by A1, A2, Th8;
hence h1 * h is_isomorphism U1,U3 by A3, A4, Th8; :: thesis: verum