let F be Field; :: thesis: for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . (a,((ovf F) . (b,c))) = (omf 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,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)
let b, c be Element of NonZero F; :: thesis: (ovf F) . (a,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)
A1: (omf F) . (b,((revf F) . c)) is Element of NonZero F by REALSET2:24;
reconsider revfb = (revf F) . b as Element of F by XBOOLE_0:def 5;
thus (ovf F) . (a,((ovf F) . (b,c))) = (ovf F) . (a,((omf F) . (b,((revf F) . c)))) by Def2
.= (omf F) . (a,((revf F) . ((omf F) . (b,((revf F) . c))))) by A1, Def2
.= (omf F) . (a,((omf F) . (((revf F) . b),((revf F) . ((revf F) . c))))) by Th3
.= a * (revfb * c) by REALSET2:23
.= (a * revfb) * c by REALSET2:19
.= (omf F) . (((ovf F) . (a,b)),c) by Def2 ; :: thesis: verum