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:233
.=
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:19
.=
(f1 . x) * (((bdif (f2,h)) . 1) . x)
by A2, DIFF_1:def 7
;
A4: 1 -' 1 =
1 - 1
by XREAL_1:233
.=
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:21
.=
(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 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
.=
((bdif ((f1 (#) f2),h)) . 1) . x
by A3, A5, Th31
;
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 Th31
.=
(((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 Th31
.=
((((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:233
.=
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:19
.=
(f1 . x) * (((bdif (f2,h)) . 2) . x)
by A11, DIFF_1:def 7
;
A13: 2 -' 1 =
2 - 1
by XREAL_1:233
.=
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:23
;
A15: 2 -' 2 =
2 - 2
by XREAL_1:233
.=
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:21
.=
(((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 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
.=
((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