let F be Field; :: thesis: for a, b being Element of NonZero F holds (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a))
let a, b be Element of NonZero F; :: thesis: (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a))
reconsider revfa = (revf F) . a, revfb = (revf F) . b as Element of NonZero F ;
A1: (omf F) . (a,((revf F) . b)) is Element of NonZero F by REALSET2:24;
A2: (omf F) . (b,((revf F) . a)) is Element of NonZero F by REALSET2:24;
revfb * (b * revfa) = revfa * (b * revfb) by REALSET2:4
.= revfa * ((omf F) . (b,revfb))
.= revfa * (1. F) by REALSET2:def 6
.= (revf F) . a by REALSET2:6 ;
then (a * revfb) * (b * revfa) = a * revfa by A2, REALSET2:4
.= (omf F) . (a,revfa)
.= 1. F by REALSET2:def 6 ;
hence (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a)) by A1, A2, REALSET2:22; :: thesis: verum