let U1, U2 be Universal_Algebra; :: thesis: for f being Function of U1,U2 st f is_isomorphism U1,U2 holds
( dom f = the carrier of U1 & rng f = the carrier of U2 )
let f be Function of U1,U2; :: thesis: ( f is_isomorphism U1,U2 implies ( dom f = the carrier of U1 & rng f = the carrier of U2 ) )
assume f is_isomorphism U1,U2 ; :: thesis: ( dom f = the carrier of U1 & rng f = the carrier of U2 )
then f is_epimorphism U1,U2 by Def4;
hence ( dom f = the carrier of U1 & rng f = the carrier of U2 ) by Def3, FUNCT_2:def 1; :: thesis: verum