:: deftheorem Def4 defines -isomorphic RING_3:def 4 :
for R, S being Ring holds
( S is R -isomorphic iff ex f being Function of R,S st
( f is RingHomomorphism & f is isomorphism ) );