let U1 be Universal_Algebra; :: thesis: U1,U1 are_isomorphic
set i = id the carrier of U1;
( id the carrier of U1 is_homomorphism U1,U1 & rng (id the carrier of U1) = the carrier of U1 ) by Th6, RELAT_1:71;
then id the carrier of U1 is_isomorphism U1,U1 by Th8;
hence U1,U1 are_isomorphic by Def5; :: thesis: verum