let F be Field; :: thesis: for a, b being Element of NonZero F holds (ovf F) . (((revf F) . a),b) = (revf F) . ((omf F) . (a,b))
let a, b be Element of NonZero F; :: thesis: (ovf F) . (((revf F) . a),b) = (revf F) . ((omf F) . (a,b))
(revf F) . a is Element of F by XBOOLE_0:def 5;
hence (ovf F) . (((revf F) . a),b) = (omf F) . (((revf F) . a),((revf F) . b)) by Def2
.= (revf F) . ((omf F) . (a,b)) by Th3 ;
:: thesis: verum