:: deftheorem Def2 defines ovf REALSET3:def 2 :
for F being Field
for b₂ being Function of [: the carrier of F,(NonZero F):], the carrier of F holds
( b₂ = ovf F iff for x being Element of F
for y being Element of NonZero F holds b₂ . (x,y) = (omf F) . (x,((revf F) . y)) );