let F be Field; :: thesis: for a, b being Element of NonZero F holds (revf F) . ((omf F) . (a,b)) = (omf F) . (((revf F) . a),((revf F) . b))
let a, b be Element of NonZero F; :: thesis: (revf F) . ((omf F) . (a,b)) = (omf F) . (((revf F) . a),((revf F) . b))
reconsider revfa = (revf F) . a, revfb = (revf F) . b as Element of NonZero F ;
thus (revf F) . ((omf F) . (a,b)) = (revf F) . ((omf F) . (a,((revf F) . ((revf F) . b)))) by REALSET2:23
.= revfb * revfa by Th2
.= revfa * revfb
.= (omf F) . (((revf F) . a),((revf F) . b)) ; :: thesis: verum