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

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