theorem :: REALSET3:6

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