take R ; :: thesis: R is R -homomorphic
take id R ; :: according to RING_2:def 4 :: thesis: id R is RingHomomorphism
thus id R is RingHomomorphism ; :: thesis: verum