let h, x be Real; :: thesis:
let f1, f2 be Function of REAL ,REAL ; :: thesis:
let S be Seq_Sequence; :: thesis:
A1: 1 -' 0 = 1 - 0 by XREAL_1:235
.= 1 ;
A2: 1 -' 1 = 1 - 1 by XREAL_1:235
.= 0 ;
A3: (fdif (f1 (#) f2),h) . 1 is Function of REAL ,REAL by Th2;
A4: 2 -' 1 = 2 - 1 by XREAL_1:235
.= 1 ;
A5: (fdif f2,h) . 1 is Function of REAL ,REAL by Th2;
A6: 2 -' 2 = 2 - 2 by XREAL_1:235
.= 0 ;
assume A7: for n, i being Element of 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:
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:33 ;
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:31
.= (((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:29
.= (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 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
.= ((fdif (f1 (#) f2),h) . 1) . x by A10, A9, Lm5 ;
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 Lm5
.= (((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 Lm5
.= ((((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:235
.= 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:31
.= (((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:29
.= (f1 . x) * (((fdif f2,h) . 2) . x) by A14, Def6 ;
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
.= ((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; :: thesis: