let UA be Universal_Algebra; :: thesis: id the carrier of UA is_isomorphism UA,UA
set I = id the carrier of UA;
id the carrier of UA is_homomorphism UA,UA by ALG_1:5;
hence id the carrier of UA is_monomorphism UA,UA by ALG_1:def 2; :: according to ALG_1:def 4 :: thesis: id the carrier of UA is_epimorphism UA,UA
( id the carrier of UA is_homomorphism UA,UA & rng (id the carrier of UA) = the carrier of UA ) by ALG_1:5, RELAT_1:45;
hence id the carrier of UA is_epimorphism UA,UA by ALG_1:def 3; :: thesis: verum