let F be Field; :: thesis: for a being Element of the carrier of F
for b, c being Element of NonZero F holds (ovf F) . a,((omf F) . b,c) = (ovf F) . ((ovf F) . a,b),c
let a be Element of the carrier of F; :: thesis: for b, c being Element of NonZero F holds (ovf F) . a,((omf F) . b,c) = (ovf F) . ((ovf F) . a,b),c
let b, c be Element of NonZero F; :: thesis: (ovf F) . a,((omf F) . b,c) = (ovf F) . ((ovf F) . a,b),c
reconsider revfb = (revf F) . b, revfc = (revf F) . c as Element of F by XBOOLE_0:def 5;
(omf F) . b,c is Element of NonZero F by REALSET2:28;
hence (ovf F) . a,((omf F) . b,c) = (omf F) . a,((revf F) . ((omf F) . b,c)) by Def2
.= a * (revfb * revfc) by Th6
.= (a * revfb) * revfc by REALSET2:23
.= (omf F) . ((ovf F) . a,b),((revf F) . c) by Def2
.= (ovf F) . ((ovf F) . a,b),c by Def2 ;
:: thesis: verum