let h, x be Real; for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
let f1, f2 be Function of REAL,REAL; for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
let S be Seq_Sequence; ( ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) implies ( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) )
assume A1:
for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2))))
; ( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
A2: 1 -' 0 =
1 - 0
by XREAL_1:233
.=
1
;
A3: (S . 1) . 0 =
((1 choose 0) * (((cdif (f1,h)) . 0) . (x + ((1 -' 0) * (h / 2))))) * (((cdif (f2,h)) . (1 -' 0)) . (x - (0 * (h / 2))))
by A1
.=
(1 * (((cdif (f1,h)) . 0) . (x + ((1 -' 0) * (h / 2))))) * (((cdif (f2,h)) . (1 -' 0)) . (x - (0 * (h / 2))))
by NEWTON:19
.=
(f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)
by A2, DIFF_1:def 8
;
A4: 1 -' 1 =
1 - 1
by XREAL_1:233
.=
0
;
A5: (S . 1) . 1 =
((1 choose 1) * (((cdif (f1,h)) . 1) . (x + ((1 -' 1) * (h / 2))))) * (((cdif (f2,h)) . (1 -' 1)) . (x - (1 * (h / 2))))
by A1
.=
(1 * (((cdif (f1,h)) . 1) . (x + ((1 -' 1) * (h / 2))))) * (((cdif (f2,h)) . (1 -' 1)) . (x - (1 * (h / 2))))
by NEWTON:21
.=
(f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x)
by A4, DIFF_1:def 8
;
A6: Sum ((S . 1),1) =
(Partial_Sums (S . 1)) . (0 + 1)
by SERIES_1:def 5
.=
((Partial_Sums (S . 1)) . 0) + ((S . 1) . 1)
by SERIES_1:def 1
.=
((S . 1) . 0) + ((S . 1) . 1)
by SERIES_1:def 1
.=
((cdif ((f1 (#) f2),h)) . 1) . x
by A3, A5, Th34
;
A7:
(cdif ((f1 (#) f2),h)) . 1 is Function of REAL,REAL
by DIFF_1:19;
A8:
(cdif (f1,h)) . 1 is Function of REAL,REAL
by DIFF_1:19;
A9:
(cdif (f2,h)) . 1 is Function of REAL,REAL
by DIFF_1:19;
A10: ((cdif ((f1 (#) f2),h)) . 2) . x =
((cdif ((f1 (#) f2),h)) . (1 + 1)) . x
.=
(cD (((cdif ((f1 (#) f2),h)) . 1),h)) . x
by DIFF_1:def 8
.=
(((cdif ((f1 (#) f2),h)) . 1) . (x + (h / 2))) - (((cdif ((f1 (#) f2),h)) . 1) . (x - (h / 2)))
by A7, DIFF_1:5
.=
(((f1 . ((x + (h / 2)) + (h / 2))) * (((cdif (f2,h)) . 1) . (x + (h / 2)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (f2 . ((x + (h / 2)) - (h / 2))))) - (((cdif ((f1 (#) f2),h)) . 1) . (x - (h / 2)))
by Th34
.=
(((f1 . (x + h)) * (((cdif (f2,h)) . 1) . (x + (h / 2)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (f2 . x))) - (((f1 . ((x - (h / 2)) + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2)))) + ((((cdif (f1,h)) . 1) . (x - (h / 2))) * (f2 . ((x - (h / 2)) - (h / 2)))))
by Th34
.=
((((f1 . (x + h)) * ((((cdif (f2,h)) . 1) . (x + (h / 2))) - (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((f1 . (x + h)) - (f1 . x)) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) - (((((cdif (f1,h)) . 1) . (x - (h / 2))) - (((cdif (f1,h)) . 1) . (x + (h / 2)))) * (f2 . (x - h)))) - ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x)))
.=
((((f1 . (x + h)) * ((cD (((cdif (f2,h)) . 1),h)) . x)) + (((f1 . ((x + (h / 2)) + (h / 2))) - (f1 . ((x + (h / 2)) - (h / 2)))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) - (((((cdif (f1,h)) . 1) . (x - (h / 2))) - (((cdif (f1,h)) . 1) . (x + (h / 2)))) * (f2 . (x - h)))) - ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x)))
by A9, DIFF_1:5
.=
((((f1 . (x + h)) * ((cD (((cdif (f2,h)) . 1),h)) . x)) + (((cD (f1,h)) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((((cdif (f1,h)) . 1) . (x + (h / 2))) - (((cdif (f1,h)) . 1) . (x - (h / 2)))) * (f2 . (x - h)))) - ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x)))
by DIFF_1:5
.=
((((f1 . (x + h)) * ((cD (((cdif (f2,h)) . 1),h)) . x)) + (((cD (f1,h)) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((cD (((cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . ((x - (h / 2)) + (h / 2))) - (f2 . ((x - (h / 2)) - (h / 2)))))
by A8, DIFF_1:5
.=
((((f1 . (x + h)) * ((cD (((cdif (f2,h)) . 1),h)) . x)) + (((cD (f1,h)) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((cD (((cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((cD (f2,h)) . (x - (h / 2))))
by DIFF_1:5
.=
((((f1 . (x + h)) * (((cdif (f2,h)) . (1 + 1)) . x)) + (((cD (f1,h)) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((cD (((cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((cD (f2,h)) . (x - (h / 2))))
by DIFF_1:def 8
.=
((((f1 . (x + h)) * (((cdif (f2,h)) . 2) . x)) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + (((cD (((cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((cD (f2,h)) . (x - (h / 2))))
by Th16
.=
((((f1 . (x + h)) * (((cdif (f2,h)) . 2) . x)) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + ((((cdif (f1,h)) . (1 + 1)) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * ((cD (f2,h)) . (x - (h / 2))))
by DIFF_1:def 8
.=
((((f1 . (x + h)) * (((cdif (f2,h)) . 2) . x)) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + ((((cdif (f1,h)) . 2) . x) * (f2 . (x - h)))) + ((((cdif (f1,h)) . 1) . (x + (h / 2))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))
by Th16
.=
(((f1 . (x + h)) * (((cdif (f2,h)) . 2) . x)) + ((2 * (((cdif (f1,h)) . 1) . (x + (h / 2)))) * (((cdif (f2,h)) . 1) . (x - (h / 2))))) + ((((cdif (f1,h)) . 2) . x) * (f2 . (x - h)))
;
A11: 2 -' 0 =
2 - 0
by XREAL_1:233
.=
2
;
A12: (S . 2) . 0 =
((2 choose 0) * (((cdif (f1,h)) . 0) . (x + ((2 -' 0) * (h / 2))))) * (((cdif (f2,h)) . (2 -' 0)) . (x - (0 * (h / 2))))
by A1
.=
(1 * (((cdif (f1,h)) . 0) . (x + ((2 -' 0) * (h / 2))))) * (((cdif (f2,h)) . (2 -' 0)) . (x - (0 * (h / 2))))
by NEWTON:19
.=
(f1 . (x + h)) * (((cdif (f2,h)) . 2) . x)
by A11, DIFF_1:def 8
;
A13: 2 -' 1 =
2 - 1
by XREAL_1:233
.=
1
;
A14: (S . 2) . 1 =
((2 choose 1) * (((cdif (f1,h)) . 1) . (x + ((2 -' 1) * (h / 2))))) * (((cdif (f2,h)) . (2 -' 1)) . (x - (1 * (h / 2))))
by A1
.=
(2 * (((cdif (f1,h)) . 1) . (x + (h / 2)))) * (((cdif (f2,h)) . 1) . (x - (h / 2)))
by A13, NEWTON:23
;
A15: 2 -' 2 =
2 - 2
by XREAL_1:233
.=
0
;
A16: (S . 2) . 2 =
((2 choose 2) * (((cdif (f1,h)) . 2) . (x + ((2 -' 2) * (h / 2))))) * (((cdif (f2,h)) . (2 -' 2)) . (x - (2 * (h / 2))))
by A1
.=
(1 * (((cdif (f1,h)) . 2) . (x + ((2 -' 2) * (h / 2))))) * (((cdif (f2,h)) . (2 -' 2)) . (x - (2 * (h / 2))))
by NEWTON:21
.=
(((cdif (f1,h)) . 2) . x) * (f2 . (x - h))
by A15, DIFF_1:def 8
;
Sum ((S . 2),2) =
(Partial_Sums (S . 2)) . (1 + 1)
by SERIES_1:def 5
.=
((Partial_Sums (S . 2)) . (0 + 1)) + ((S . 2) . 2)
by SERIES_1:def 1
.=
(((Partial_Sums (S . 2)) . 0) + ((S . 2) . 1)) + ((S . 2) . 2)
by SERIES_1:def 1
.=
((cdif ((f1 (#) f2),h)) . 2) . x
by A10, A12, A14, A16, SERIES_1:def 1
;
hence
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
by A6; verum