let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1
let h be Function of U1,U2; :: thesis: for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1
let h1 be Function of U2,U1; :: thesis: ( h is_isomorphism U1,U2 & h1 = h " implies h1 is_isomorphism U2,U1 )
assume that
A1: h is_isomorphism U1,U2 and
A2: h1 = h " ; :: thesis: h1 is_isomorphism U2,U1
A3: h1 is_homomorphism U2,U1 by A1, A2, Th10;
A4: h is one-to-one by A1, Th8;
then rng h1 = dom h by A2, FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def 1 ;
hence h1 is_isomorphism U2,U1 by A2, A4, A3, Th8; :: thesis: verum