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:25
.= (omf F) . a,(1. F)
.= a * (d * revfd) by REALSET2:def 18
.= (a * d) * revfd by REALSET2:23 ;
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;
b = b * (1. F) by REALSET2:25
.= (omf F) . b,(1. F)
.= b * (c * revfc) by REALSET2:def 18
.= (b * c) * revfc by REALSET2:23 ;
then A2: (omf F) . b,((revf F) . d) = ((b * c) * revfc) * revfd
.= (b * c) * (revfc * revfd) by REALSET2:23
.= (omf F) . ((omf F) . b,c),((revf F) . ((omf F) . c,d)) by Th6 ;
(omf F) . a,((revf F) . c) = ((a * d) * revfd) * revfc by A1
.= (a * d) * (revfd * revfc) by REALSET2:23
.= (omf F) . ((omf F) . a,d),(revfc * revfd)
.= (omf F) . ((omf F) . a,d),((revf F) . ((omf F) . c,d)) by Th6 ;
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 18
.= (omf F) . (the addF of F . ((omf F) . a,d),((omf F) . b,c)),((revf F) . ((omf F) . c,d)) ;
:: thesis: verum