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 the carrier 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 Th6 ;
:: thesis: verum