theorem Th3: :: REALSET3:3

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