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