let F be Field; 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; 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; (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
; verum