let UA be Universal_Algebra; :: thesis: id the carrier of UA in UAEnd UA
id the carrier of UA is_homomorphism by ALG_1:5;
hence id the carrier of UA in UAEnd UA by Def1; :: thesis: verum