take R ; :: thesis: ( R is R -homomorphic & R is R -isomorphic )
id R is RingHomomorphism ;
hence R is R -homomorphic ; :: thesis: R is R -isomorphic
id R is RingIsomorphism ;
hence R is R -isomorphic by RING_3:def 4; :: thesis: verum