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