let F be Field; :: thesis: for a, b being Element of the carrier of F \ {(0. F)} holds (revf F) . ((omf F) . a,b) = (omf F) . ((revf F) . a),((revf F) . b)
let a, b be Element of the carrier of F \ {(0. 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 the carrier of F \ {(0. F)} ;
thus (revf F) . ((omf F) . a,b) = (revf F) . ((omf F) . a,((revf F) . ((revf F) . b))) by REALSET2:27
.= revfb * revfa by Th4
.= revfa * revfb
.= (omf F) . ((revf F) . a),((revf F) . b) ; :: thesis: verum