consider f being Function of R,S such that
A1: ( f is RingHomomorphism & f is monomorphism ) by Def3;
take f ; :: thesis: ( f is additive & f is multiplicative & f is unity-preserving & f is monomorphism )
thus f is additive by A1; :: thesis: ( f is multiplicative & f is unity-preserving & f is monomorphism )
thus f is multiplicative by A1; :: thesis: ( f is unity-preserving & f is monomorphism )
thus f is unity-preserving by A1; :: thesis: f is monomorphism
thus f is monomorphism by A1; :: thesis: verum