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