let F be Field; 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; 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; 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))))
;
verum