:: deftheorem Def6 defines revf REALSET2:def 6 :
for F being Field
for b₂ being UnOp of (NonZero F) holds
( b₂ = revf F iff for x being Element of NonZero F holds (omf F) . (x,(b₂ . x)) = 1. F );