theorem Th25: :: REALSET3:25

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