take S ; :: thesis: ( S is S -homomorphic & S is R -homomorphic )
id S is RingHomomorphism ;
hence S is S -homomorphic by RING_2:def 4; :: thesis: S is R -homomorphic
thus S is R -homomorphic ; :: thesis: verum