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

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