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