let S be R -monomorphic Ring; :: thesis: S is R -homomorphic
ex f being Function of R,S st
( f is RingHomomorphism & f is monomorphism ) by Def3;
hence S is R -homomorphic ; :: thesis: verum