let UA be Universal_Algebra; :: thesis: for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds

g is_isomorphism

let f, g be Function of UA,UA; :: thesis: ( f is Element of UAAut UA & g = f " implies g is_isomorphism )

assume that

A1: f is Element of UAAut UA and

A2: g = f " ; :: thesis: g is_isomorphism

f is_isomorphism by A1, Def1;

hence g is_isomorphism by A2, ALG_1:10; :: thesis: verum

g is_isomorphism

let f, g be Function of UA,UA; :: thesis: ( f is Element of UAAut UA & g = f " implies g is_isomorphism )

assume that

A1: f is Element of UAAut UA and

A2: g = f " ; :: thesis: g is_isomorphism

f is_isomorphism by A1, Def1;

hence g is_isomorphism by A2, ALG_1:10; :: thesis: verum