let F be Field; :: thesis: for a, b being Element of F
for c being Element of NonZero F holds (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
let a, b be Element of F; :: thesis: for c being Element of NonZero F holds (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
let c be Element of NonZero F; :: thesis: (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
reconsider revfc = (revf F) . c as Element of F by XBOOLE_0:def 5;
thus (omf F) . (a,((ovf F) . (b,c))) = a * (b * revfc) by Def2
.= (a * b) * revfc by REALSET2:19
.= (ovf F) . (((omf F) . (a,b)),c) by Def2 ; :: thesis: verum