theorem :: REALSET3:24

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