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