let h, x be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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))) ; :: thesis: ( ((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 ;
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 ;
A10: (S . 1) . 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 ;
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
.= (((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
.= ((((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
.= ((((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 ;
A16: (S . 2) . 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 ;
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 ;
hence ( ((fdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((fdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) ) by A11; :: thesis: verum