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