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:28;
A2: (omf F) . b,((revf F) . a) is Element of NonZero F by REALSET2:28;
revfb * (b * revfa) = revfa * (b * revfb) by REALSET2:8
.= revfa * ((omf F) . b,revfb)
.= revfa * (1. F) by REALSET2:def 18
.= (revf F) . a by REALSET2:10 ;
then (a * revfb) * (b * revfa) = a * revfa by A2, REALSET2:8
.= (omf F) . a,revfa
.= 1. F by REALSET2:def 18 ;
hence (revf F) . ((omf F) . a,((revf F) . b)) = (omf F) . b,((revf F) . a) by A1, A2, REALSET2:26; :: thesis: verum