let F be Field; :: thesis: for a being Element 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 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:24;
hence (ovf F) . (a,((omf F) . (b,c))) = (omf F) . (a,((revf F) . ((omf F) . (b,c)))) by Def2
.= a * (revfb * revfc) by Th3
.= (a * revfb) * revfc by REALSET2:19
.= (omf F) . (((ovf F) . (a,b)),((revf F) . c)) by Def2
.= (ovf F) . (((ovf F) . (a,b)),c) by Def2 ;
:: thesis: verum