:: deftheorem defines is_ringisomorph_to QUOFIELD:def 23 :
for R, S being non empty doubleLoopStr holds
( R is_ringisomorph_to S iff ex f being Function of R,S st f is RingIsomorphism );