theorem Th5: :: REALSET3:5

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