:: deftheorem Def9 defines isoR FIELD_3:def 10 :
for F being non almost_trivial Field
for x being non trivial Element of F
for o being object
for b₄ being Function of F,(ExField (x,o)) holds
( b₄ = isoR (x,o) iff ( b₄ . x = o & ( for a being Element of F st a <> x holds
b₄ . a = a ) ) );