let UA be Universal_Algebra; :: thesis: id the carrier of UA is_isomorphism UA,UA
set I = id the carrier of UA;
thus id the carrier of UA is_monomorphism UA,UA :: according to ALG_1:def 4 :: thesis: id the carrier of UA is_epimorphism UA,UA

proof

thus id the carrier of UA is_homomorphism UA,UA by ALG_1:6; :: according to ALG_1:def 2 :: thesis: id the carrier of UA is one-to-one
thus id the carrier of UA is one-to-one ; :: thesis: verum

end;

thus id the carrier of UA is_epimorphism UA,UA :: thesis: verum

proof

thus id the carrier of UA is_homomorphism UA,UA by ALG_1:6; :: according to ALG_1:def 3 :: thesis: K321(the carrier of UA,the carrier of UA,(id the carrier of UA)) = the carrier of UA
thus rng (id the carrier of UA) = the carrier of UA by RELAT_1:71; :: thesis: verum

end;