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:235
.=
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:29
.=
(f1 . (x + (h / 2))) * (((cdif f2,h) . 1) . x)
by A2, DIFF_1:def 8
;
A4: 1 -' 1 =
1 - 1
by XREAL_1:235
.=
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:31
.=
(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 6
.=
((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, Th42
;
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 Th42
.=
(((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 Th42
.=
((((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 Th23
.=
((((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 Th23
.=
(((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:235
.=
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:29
.=
(f1 . (x + h)) * (((cdif f2,h) . 2) . x)
by A11, DIFF_1:def 8
;
A13: 2 -' 1 =
2 - 1
by XREAL_1:235
.=
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:33
;
A15: 2 -' 2 =
2 - 2
by XREAL_1:235
.=
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:31
.=
(((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 6
.=
((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