theorem Th2: :: REALSET3:2

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