let UA be Universal_Algebra; :: thesis: for f being Function of UA,UA st f is_isomorphism holds
f " is Function of UA,UA
let f be Function of UA,UA; :: thesis: ( f is_isomorphism implies f " is Function of UA,UA )
assume A1: f is_isomorphism ; :: thesis: f " is Function of UA,UA
then f is_epimorphism ;
then A2: rng f = the carrier of UA ;
f is one-to-one by A1, ALG_1:7;
hence f " is Function of UA,UA by A2, FUNCT_2:25; :: thesis: verum