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) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) holds
( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((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) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) holds
( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((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) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h))) ) implies ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) )
A1: 1 -' 0 =
1 - 0
by XREAL_1:233
.=
1
;
A2: 1 -' 1 =
1 - 1
by XREAL_1:233
.=
0
;
A3:
(fdif ((f1 (#) f2),h)) . 1 is Function of REAL,REAL
by Th2;
A4: 2 -' 1 =
2 - 1
by XREAL_1:233
.=
1
;
A5:
(fdif (f2,h)) . 1 is Function of REAL,REAL
by Th2;
A6: 2 -' 2 =
2 - 2
by XREAL_1:233
.=
0
;
assume A7:
for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((fdif (f1,h)) . i) . x)) * (((fdif (f2,h)) . (n -' i)) . (x + (i * h)))
; ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
then A8: (S . 2) . 1 =
((2 choose 1) * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (2 -' 1)) . (x + (1 * h)))
.=
(2 * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . 1) . (x + h))
by A4, NEWTON:23
;
A9: (S . 1) . 1 =
((1 choose 1) * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (1 -' 1)) . (x + (1 * h)))
by A7
.=
(1 * (((fdif (f1,h)) . 1) . x)) * (((fdif (f2,h)) . (1 -' 1)) . (x + (1 * h)))
by NEWTON:21
.=
(((fdif (f1,h)) . 1) . x) * (f2 . (x + h))
by A2, Def6
;
A10: (S . 1) . 0 =
((1 choose 0) * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (1 -' 0)) . (x + (0 * h)))
by A7
.=
(1 * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (1 -' 0)) . (x + (0 * h)))
by NEWTON:19
.=
(f1 . x) * (((fdif (f2,h)) . 1) . x)
by A1, Def6
;
A11: 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
.=
((fdif ((f1 (#) f2),h)) . 1) . x
by A10, A9, Lm2
;
A12:
(fdif (f1,h)) . 1 is Function of REAL,REAL
by Th2;
A13: ((fdif ((f1 (#) f2),h)) . 2) . x =
((fdif ((f1 (#) f2),h)) . (1 + 1)) . x
.=
(fD (((fdif ((f1 (#) f2),h)) . 1),h)) . x
by Def6
.=
(((fdif ((f1 (#) f2),h)) . 1) . (x + h)) - (((fdif ((f1 (#) f2),h)) . 1) . x)
by A3, Th3
.=
(((f1 . (x + h)) * (((fdif (f2,h)) . 1) . (x + h))) + ((((fdif (f1,h)) . 1) . (x + h)) * (f2 . ((x + h) + h)))) - (((fdif ((f1 (#) f2),h)) . 1) . x)
by Lm2
.=
(((f1 . (x + h)) * (((fdif (f2,h)) . 1) . (x + h))) + ((((fdif (f1,h)) . 1) . (x + h)) * (f2 . ((x + h) + h)))) - (((f1 . x) * (((fdif (f2,h)) . 1) . x)) + ((((fdif (f1,h)) . 1) . x) * (f2 . (x + h))))
by Lm2
.=
((((f1 . x) * ((((fdif (f2,h)) . 1) . (x + h)) - (((fdif (f2,h)) . 1) . x))) + (((f1 . (x + h)) - (f1 . x)) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h))))
.=
((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((f1 . (x + h)) - (f1 . x)) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h))))
by A5, Th3
.=
((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((((fdif (f1,h)) . 1) . (x + h)) - (((fdif (f1,h)) . 1) . x)) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h))))
by Th3
.=
((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((f2 . ((x + h) + h)) - (f2 . (x + h))))
by A12, Th3
.=
((((f1 . x) * ((fD (((fdif (f2,h)) . 1),h)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h)))
by Th3
.=
((((f1 . x) * (((fdif (f2,h)) . (1 + 1)) . x)) + (((fD (f1,h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h)))
by Def6
.=
((((f1 . x) * (((fdif (f2,h)) . (1 + 1)) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + (((fD (((fdif (f1,h)) . 1),h)) . x) * (f2 . ((x + h) + h)))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h)))
by Def6
.=
((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + (((fD (((fdif (f1,h)) . 0),h)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h)))
by Def6
.=
((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . (0 + 1)) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (f2,h)) . (x + h)))
by Def6
.=
((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * ((fD (((fdif (f2,h)) . 0),h)) . (x + h)))
by Def6
.=
((((f1 . x) * (((fdif (f2,h)) . 2) . x)) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h)))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))) + ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . (0 + 1)) . (x + h)))
by Def6
.=
(((f1 . x) * (((fdif (f2,h)) . 2) . x)) + (2 * ((((fdif (f1,h)) . 1) . x) * (((fdif (f2,h)) . 1) . (x + h))))) + ((((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h))))
;
A14: 2 -' 0 =
2 - 0
by XREAL_1:233
.=
2
;
A15: (S . 2) . 2 =
((2 choose 2) * (((fdif (f1,h)) . 2) . x)) * (((fdif (f2,h)) . (2 -' 2)) . (x + (2 * h)))
by A7
.=
(1 * (((fdif (f1,h)) . 2) . x)) * (((fdif (f2,h)) . (2 -' 2)) . (x + (2 * h)))
by NEWTON:21
.=
(((fdif (f1,h)) . 2) . x) * (f2 . (x + (2 * h)))
by A6, Def6
;
A16: (S . 2) . 0 =
((2 choose 0) * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (2 -' 0)) . (x + (0 * h)))
by A7
.=
(1 * (((fdif (f1,h)) . 0) . x)) * (((fdif (f2,h)) . (2 -' 0)) . (x + (0 * h)))
by NEWTON:19
.=
(f1 . x) * (((fdif (f2,h)) . 2) . x)
by A14, Def6
;
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
.=
((fdif ((f1 (#) f2),h)) . 2) . x
by A13, A16, A8, A15, SERIES_1:def 1
;
hence
( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
by A11; verum