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