let F be Field; :: thesis: for a, b being Element of F
for c, d being Element of NonZero F holds (omf F) . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (((omf F) . (a,b)),((revf F) . ((omf F) . (c,d))))
let a, b be Element of F; :: thesis: for c, d being Element of NonZero F holds (omf F) . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (((omf F) . (a,b)),((revf F) . ((omf F) . (c,d))))
let c, d be Element of NonZero F; :: thesis: (omf F) . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (((omf F) . (a,b)),((revf F) . ((omf F) . (c,d))))
reconsider revfc = (revf F) . c, revfd = (revf F) . d as Element of NonZero F ;
(omf F) . (c,d) is Element of NonZero F by REALSET2:24;
then reconsider revfcd = (revf F) . (c * d) as Element of F by REALSET2:24;
thus (omf F) . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (a * revfc) * (b * revfd)
.= a * (revfc * (b * revfd)) by REALSET2:19
.= a * (b * (revfc * revfd)) by REALSET2:19
.= (omf F) . (a,((omf F) . (b,((revf F) . ((omf F) . (c,d)))))) by Th3
.= a * (b * revfcd)
.= (a * b) * revfcd by REALSET2:19
.= (omf F) . (((omf F) . (a,b)),((revf F) . ((omf F) . (c,d)))) ; :: thesis: verum