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:28;
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 Th6
.= a * (revfb * c) by REALSET2:27
.= (a * revfb) * c by REALSET2:23
.= (omf F) . ((ovf F) . a,b),c by Def2 ; :: thesis: verum