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