let UA be Universal_Algebra; :: thesis: for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA
let f1, f2 be Element of UAAut UA; :: thesis: f1 * f2 in UAAut UA
( f1 is_isomorphism UA,UA & f2 is_isomorphism UA,UA ) by Def1;
then f1 * f2 is_isomorphism UA,UA by ALG_1:12;
hence f1 * f2 in UAAut UA by Def1; :: thesis: verum