let F be Field; :: thesis: for a, b being Element of F
for c, d being Element of NonZero F holds the addF of F . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (( the addF of F . (((omf F) . (a,d)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,d))))
let a, b be Element of F; :: thesis: for c, d being Element of NonZero F holds the addF of F . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (( the addF of F . (((omf F) . (a,d)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,d))))
let c, d be Element of NonZero F; :: thesis: the addF of F . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = (omf F) . (( the addF of F . (((omf F) . (a,d)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,d))))
reconsider revfd = (revf F) . d as Element of F by XBOOLE_0:def 5;
A1: a = a * (1. F) by REALSET2:21
.= (omf F) . (a,(1. F))
.= a * (d * revfd) by REALSET2:def 6
.= (a * d) * revfd by REALSET2:19 ;
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;
b = b * (1. F) by REALSET2:21
.= (omf F) . (b,(1. F))
.= b * (c * revfc) by REALSET2:def 6
.= (b * c) * revfc by REALSET2:19 ;
then A2: (omf F) . (b,((revf F) . d)) = ((b * c) * revfc) * revfd
.= (b * c) * (revfc * revfd) by REALSET2:19
.= (omf F) . (((omf F) . (b,c)),((revf F) . ((omf F) . (c,d)))) by Th3 ;
(omf F) . (a,((revf F) . c)) = ((a * d) * revfd) * revfc by A1
.= (a * d) * (revfd * revfc) by REALSET2:19
.= (omf F) . (((omf F) . (a,d)),(revfc * revfd))
.= (omf F) . (((omf F) . (a,d)),((revf F) . ((omf F) . (c,d)))) by Th3 ;
hence the addF of F . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . d)))) = ((a * d) * revfcd) + ((b * c) * revfcd) by A2
.= ((a * d) + (b * c)) * revfcd by VECTSP_1:def 7
.= (omf F) . (( the addF of F . (((omf F) . (a,d)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,d)))) ;
:: thesis: verum