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:6;
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:6, RELAT_1:71;
hence id the carrier of UA is_epimorphism UA,UA by ALG_1:def 3; :: thesis: verum