:: deftheorem defines -isomorphism FIELD_8:def 8 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Relation of the carrier of S1, the carrier of S2 holds
( h is R -isomorphism iff ex g being Function of S1,S2 st
( g = h & g is R -isomorphism ) );