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 UA,UA
let f, g be Function of UA,UA; :: thesis: ( f is Element of UAAut UA & g = f " implies g is_isomorphism UA,UA )
assume that
A1: f is Element of UAAut UA and
A2: g = f " ; :: thesis: g is_isomorphism UA,UA
f is_isomorphism UA,UA by A1, Def1;
hence g is_isomorphism UA,UA by A2, ALG_1:10; :: thesis: verum