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