let U1 be Universal_Algebra; :: thesis: U1,U1 are_isomorphic
set i = id the carrier of U1;
( id the carrier of U1 is_homomorphism & rng (id the carrier of U1) = the carrier of U1 ) by Th5;
then id the carrier of U1 is_isomorphism by Th7;
hence U1,U1 are_isomorphic ; :: thesis: verum