let F be Field; :: thesis: for a, b being Element of the carrier 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 the carrier 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:28;
then reconsider revfcd = (revf F) . (c * d) as Element of F by REALSET2:28;
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:23
.= a * (b * (revfc * revfd)) by REALSET2:23
.= (omf F) . a,((omf F) . b,((revf F) . ((omf F) . c,d))) by Th6
.= a * (b * revfcd)
.= (a * b) * revfcd by REALSET2:23
.= (omf F) . ((omf F) . a,b),((revf F) . ((omf F) . c,d)) ; :: thesis: verum