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