theorem :: REALSET3:23

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