let F, G be Field; :: thesis: for V being VectSp of F
for W being VectSp of G
for f being Function of V,W
for x, h being Element of V
for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
let V be VectSp of F; :: thesis: for W being VectSp of G
for f being Function of V,W
for x, h being Element of V
for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
let W be VectSp of G; :: thesis: for f being Function of V,W
for x, h being Element of V
for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
let f be Function of V,W; :: thesis: for x, h being Element of V
for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
let x, h be Element of V; :: thesis: for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
let n be Nat; :: thesis: ( 1. F <> - (1. F) implies ((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h)) )
assume AS: 1. F <> - (1. F) ; :: thesis: ((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))
A32: (1. F) + (1. F) = (1 * (1. F)) + (1. F) by BINOM:13
.= (1 * (1. F)) + (1 * (1. F)) by BINOM:13
.= (1 + 1) * (1. F) by BINOM:15
.= 2 * (1. F) ;
A33: h + h = ((1. F) * h) + h
.= ((1. F) * h) + ((1. F) * h)
.= (2 * (1. F)) * h by A32, VECTSP_1:def 15 ;
A30: 2 * (1. F) <> 0. F

proof

assume A301: 2 * (1. F) = 0. F ; :: thesis: contradiction
(1. F) + (1. F) = (1 * (1. F)) + (1. F) by BINOM:13
.= (1 * (1. F)) + (1 * (1. F)) by BINOM:13
.= (1 + 1) * (1. F) by BINOM:15
.= 0. F by A301 ;
hence contradiction by AS, RLVECT_1:def 10; :: thesis: verum

end;

A34: (((2 * (1. F)) ") * h) + (((2 * (1. F)) ") * h) = ((2 * (1. F)) ") * (h + h) by VECTSP_1:def 14
.= (((2 * (1. F)) ") * (2 * (1. F))) * h by VECTSP_1:def 16, A33
.= (1. F) * h by A30, VECTSP_1:def 10
.= h ;
A52: (cdif (f,h)) . (2 * n) is Function of V,W by Th19;
A35: ((x + (n * h)) + (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h) = (x + (n * h)) + ((((2 * (1. F)) ") * h) - (((2 * (1. F)) ") * h)) by RLVECT_1:28
.= (x + (n * h)) + (0. V) by RLVECT_1:15
.= x + (n * h) by RLVECT_1:4 ;
A36: ((x + (n * h)) + (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h) = (x + (n * h)) + ((((2 * (1. F)) ") * h) + (((2 * (1. F)) ") * h)) by RLVECT_1:def 3
.= x + ((n * h) + h) by RLVECT_1:def 3, A34
.= x + ((n * h) + (1 * h)) by BINOM:13
.= x + ((n + 1) * h) by BINOM:15 ;
A51: (fdif (f,h)) . (2 * n) is Function of V,W by Th2;
A11: ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h)) = (cD (((cdif (f,h)) . (2 * n)),h)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h)) by Def8
.= (((cdif (f,h)) . (2 * n)) /. (x + ((n + 1) * h))) - (((cdif (f,h)) . (2 * n)) /. (((x + (n * h)) + (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h))) by A36, Th5, A52
.= (((cdif (f,h)) . (2 * n)) /. (x + ((n * h) + (1 * h)))) - (((cdif (f,h)) . (2 * n)) /. (x + (n * h))) by BINOM:15, A35
.= (((cdif (f,h)) . (2 * n)) /. (x + ((n * h) + h))) - (((cdif (f,h)) . (2 * n)) /. (x + (n * h))) by BINOM:13
.= (((cdif (f,h)) . (2 * n)) /. ((x + h) + (n * h))) - (((cdif (f,h)) . (2 * n)) /. (x + (n * h))) by RLVECT_1:def 3
.= (((fdif (f,h)) . (2 * n)) /. (x + h)) - (((cdif (f,h)) . (2 * n)) /. (x + (n * h))) by LAST0, AS
.= (((fdif (f,h)) . (2 * n)) /. (x + h)) - (((fdif (f,h)) . (2 * n)) /. x) by LAST0, AS ;
((fdif (f,h)) . ((2 * n) + 1)) /. x = (fD (((fdif (f,h)) . (2 * n)),h)) /. x by Def6
.= (((fdif (f,h)) . (2 * n)) /. (x + h)) - (((fdif (f,h)) . (2 * n)) /. x) by Th3, A51 ;
hence ((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h)) by A11; :: thesis: verum