let UA be Universal_Algebra; :: thesis: for f being Element of UAAut UA holds f " in UAAut UA
let f be Element of UAAut UA; :: thesis: f " in UAAut UA
A1: f is_isomorphism by Def1;
then f " is Function of UA,UA by Lm1;
then consider ff being Function of UA,UA such that
A2: ff = f " ;
ff is_isomorphism by A1, A2, ALG_1:10;
hence f " in UAAut UA by A2, Def1; :: thesis: verum