theorem :: REALSET3:28

for F being Field
for a being Element of NonZero F
for b, c being Element of F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b )