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 & f2 is_isomorphism ) by Def1;
then f1 * f2 is_isomorphism by ALG_1:11;
hence f1 * f2 in UAAut UA by Def1; :: thesis: verum