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) * (((bdif f1,h) . i) . x)) * (((bdif f2,h) . (n -' i)) . (x - (i * h))) ) holds
( ((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 & ((bdif (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) * (((bdif f1,h) . i) . x)) * (((bdif f2,h) . (n -' i)) . (x - (i * h))) ) holds
( ((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 & ((bdif (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) * (((bdif f1,h) . i) . x)) * (((bdif f2,h) . (n -' i)) . (x - (i * h))) ) implies ( ((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 & ((bdif (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) * (((bdif f1,h) . i) . x)) * (((bdif f2,h) . (n -' i)) . (x - (i * h)))
; ( ((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 & ((bdif (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 ) * (((bdif f1,h) . 0 ) . x)) * (((bdif f2,h) . (1 -' 0 )) . (x - (0 * h)))
by A1
.=
(1 * (((bdif f1,h) . 0 ) . x)) * (((bdif f2,h) . (1 -' 0 )) . (x - (0 * h)))
by NEWTON:29
.=
(f1 . x) * (((bdif f2,h) . 1) . x)
by A2, DIFF_1:def 7
;
A4: 1 -' 1 =
1 - 1
by XREAL_1:235
.=
0
;
A5: (S . 1) . 1 =
((1 choose 1) * (((bdif f1,h) . 1) . x)) * (((bdif f2,h) . (1 -' 1)) . (x - (1 * h)))
by A1
.=
(1 * (((bdif f1,h) . 1) . x)) * (((bdif f2,h) . (1 -' 1)) . (x - (1 * h)))
by NEWTON:31
.=
(f2 . (x - h)) * (((bdif f1,h) . 1) . x)
by A4, DIFF_1:def 7
;
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
.=
((bdif (f1 (#) f2),h) . 1) . x
by A3, A5, Th38
;
A7:
(bdif (f1 (#) f2),h) . 1 is Function of REAL ,REAL
by DIFF_1:12;
A8:
(bdif f2,h) . 1 is Function of REAL ,REAL
by DIFF_1:12;
A9:
(bdif f1,h) . 1 is Function of REAL ,REAL
by DIFF_1:12;
A10: ((bdif (f1 (#) f2),h) . 2) . x =
((bdif (f1 (#) f2),h) . (1 + 1)) . x
.=
(bD ((bdif (f1 (#) f2),h) . 1),h) . x
by DIFF_1:def 7
.=
(((bdif (f1 (#) f2),h) . 1) . x) - (((bdif (f1 (#) f2),h) . 1) . (x - h))
by A7, DIFF_1:4
.=
(((f1 . x) * (((bdif f2,h) . 1) . x)) + ((((bdif f1,h) . 1) . x) * (f2 . (x - h)))) - (((bdif (f1 (#) f2),h) . 1) . (x - h))
by Th38
.=
(((f1 . x) * (((bdif f2,h) . 1) . x)) + ((((bdif f1,h) . 1) . x) * (f2 . (x - h)))) - (((f1 . (x - h)) * (((bdif f2,h) . 1) . (x - h))) + ((((bdif f1,h) . 1) . (x - h)) * (f2 . ((x - h) - h))))
by Th38
.=
((((f1 . x) * ((((bdif f2,h) . 1) . x) - (((bdif f2,h) . 1) . (x - h)))) + (((f1 . x) - (f1 . (x - h))) * (((bdif f2,h) . 1) . (x - h)))) - (((((bdif f1,h) . 1) . (x - h)) - (((bdif f1,h) . 1) . x)) * (f2 . (x - (2 * h))))) - ((((bdif f1,h) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h))))
.=
((((f1 . x) * ((bD ((bdif f2,h) . 1),h) . x)) + (((f1 . x) - (f1 . (x - h))) * (((bdif f2,h) . 1) . (x - h)))) - (((((bdif f1,h) . 1) . (x - h)) - (((bdif f1,h) . 1) . x)) * (f2 . (x - (2 * h))))) - ((((bdif f1,h) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h))))
by A8, DIFF_1:4
.=
((((f1 . x) * ((bD ((bdif f2,h) . 1),h) . x)) + (((bD f1,h) . x) * (((bdif f2,h) . 1) . (x - h)))) + (((((bdif f1,h) . 1) . x) - (((bdif f1,h) . 1) . (x - h))) * (f2 . (x - (2 * h))))) - ((((bdif f1,h) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h))))
by DIFF_1:4
.=
((((f1 . x) * ((bD ((bdif f2,h) . 1),h) . x)) + (((bD f1,h) . x) * (((bdif f2,h) . 1) . (x - h)))) + (((bD ((bdif f1,h) . 1),h) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((f2 . (x - h)) - (f2 . ((x - h) - h))))
by A9, DIFF_1:4
.=
((((f1 . x) * ((bD ((bdif f2,h) . 1),h) . x)) + (((bD f1,h) . x) * (((bdif f2,h) . 1) . (x - h)))) + (((bD ((bdif f1,h) . 1),h) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD f2,h) . (x - h)))
by DIFF_1:4
.=
((((f1 . x) * (((bdif f2,h) . (1 + 1)) . x)) + (((bD f1,h) . x) * (((bdif f2,h) . 1) . (x - h)))) + (((bD ((bdif f1,h) . 1),h) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD f2,h) . (x - h)))
by DIFF_1:def 7
.=
((((f1 . x) * (((bdif f2,h) . (1 + 1)) . x)) + (((bD ((bdif f1,h) . 0 ),h) . x) * (((bdif f2,h) . 1) . (x - h)))) + (((bD ((bdif f1,h) . 1),h) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD f2,h) . (x - h)))
by DIFF_1:def 7
.=
((((f1 . x) * (((bdif f2,h) . 2) . x)) + (((bD ((bdif f1,h) . 0 ),h) . x) * (((bdif f2,h) . 1) . (x - h)))) + ((((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD f2,h) . (x - h)))
by DIFF_1:def 7
.=
((((f1 . x) * (((bdif f2,h) . 2) . x)) + ((((bdif f1,h) . (0 + 1)) . x) * (((bdif f2,h) . 1) . (x - h)))) + ((((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD f2,h) . (x - h)))
by DIFF_1:def 7
.=
((((f1 . x) * (((bdif f2,h) . 2) . x)) + ((((bdif f1,h) . 1) . x) * (((bdif f2,h) . 1) . (x - h)))) + ((((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * ((bD ((bdif f2,h) . 0 ),h) . (x - h)))
by DIFF_1:def 7
.=
((((f1 . x) * (((bdif f2,h) . 2) . x)) + ((((bdif f1,h) . 1) . x) * (((bdif f2,h) . 1) . (x - h)))) + ((((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h))))) + ((((bdif f1,h) . 1) . x) * (((bdif f2,h) . (0 + 1)) . (x - h)))
by DIFF_1:def 7
.=
(((f1 . x) * (((bdif f2,h) . 2) . x)) + (2 * ((((bdif f1,h) . 1) . x) * (((bdif f2,h) . 1) . (x - h))))) + ((((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h))))
;
A11: 2 -' 0 =
2 - 0
by XREAL_1:235
.=
2
;
A12: (S . 2) . 0 =
((2 choose 0 ) * (((bdif f1,h) . 0 ) . x)) * (((bdif f2,h) . (2 -' 0 )) . (x - (0 * h)))
by A1
.=
(1 * (((bdif f1,h) . 0 ) . x)) * (((bdif f2,h) . (2 -' 0 )) . (x - (0 * h)))
by NEWTON:29
.=
(f1 . x) * (((bdif f2,h) . 2) . x)
by A11, DIFF_1:def 7
;
A13: 2 -' 1 =
2 - 1
by XREAL_1:235
.=
1
;
A14: (S . 2) . 1 =
((2 choose 1) * (((bdif f1,h) . 1) . x)) * (((bdif f2,h) . (2 -' 1)) . (x - (1 * h)))
by A1
.=
(2 * (((bdif f1,h) . 1) . x)) * (((bdif f2,h) . 1) . (x - h))
by A13, NEWTON:33
;
A15: 2 -' 2 =
2 - 2
by XREAL_1:235
.=
0
;
A16: (S . 2) . 2 =
((2 choose 2) * (((bdif f1,h) . 2) . x)) * (((bdif f2,h) . (2 -' 2)) . (x - (2 * h)))
by A1
.=
(1 * (((bdif f1,h) . 2) . x)) * (((bdif f2,h) . (2 -' 2)) . (x - (2 * h)))
by NEWTON:31
.=
(((bdif f1,h) . 2) . x) * (f2 . (x - (2 * h)))
by A15, DIFF_1:def 7
;
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
.=
((bdif (f1 (#) f2),h) . 2) . x
by A10, A12, A14, A16, SERIES_1:def 1
;
hence
( ((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 & ((bdif (f1 (#) f2),h) . 2) . x = Sum (S . 2),2 )
by A6; verum