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)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * 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)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * 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)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * 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)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))
let x, h be Element of V; :: thesis: for n being Nat st 1. F <> - (1. F) holds
((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))
let n be Nat; :: thesis: ( 1. F <> - (1. F) implies ((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h)) )
assume AS: 1. F <> - (1. F) ; :: thesis: ((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))
defpred S₁[ Nat] means for x being Element of V holds ((fdif (f,h)) . (2 * $1)) /. x = ((cdif (f,h)) . (2 * $1)) /. (x + ($1 * h));
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for x being Element of V holds ((fdif (f,h)) . (2 * k)) /. x = ((cdif (f,h)) . (2 * k)) /. (x + (k * h)) ; :: thesis: S₁[k + 1]
let x be Element of V; :: thesis: ((fdif (f,h)) . (2 * (k + 1))) /. x = ((cdif (f,h)) . (2 * (k + 1))) /. (x + ((k + 1) * h))
A31: h + h = (1 * h) + h by BINOM:13
.= (1 * h) + (1 * h) by BINOM:13
.= (1 + 1) * h by BINOM:15 ;
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 ;
A35: ((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h) = ((x + ((k * h) + (1 * h))) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h) by BINOM:15
.= (((x + (k * h)) + (1 * h)) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h) by RLVECT_1:def 3
.= (((x + (k * h)) + h) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h) by BINOM:13
.= ((x + (k * h)) + h) - ((((2 * (1. F)) ") * h) + (((2 * (1. F)) ") * h)) by RLVECT_1:27
.= (x + (k * h)) + (h - h) by RLVECT_1:28, A34
.= (x + (k * h)) + (0. V) by RLVECT_1:15
.= x + (k * h) by RLVECT_1:4 ;
A36: ((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h) = (x + ((k + 1) * h)) + ((((2 * (1. F)) ") * h) + (((2 * (1. F)) ") * h)) by RLVECT_1:def 3
.= x + (((k + 1) * h) + h) by RLVECT_1:def 3, A34
.= x + (((k + 1) * h) + (1 * h)) by BINOM:13
.= x + (((k + 1) + 1) * h) by BINOM:15
.= x + ((k + 2) * h) ;
A3: ((fdif (f,h)) . (2 * k)) /. ((x + h) + h) = ((cdif (f,h)) . (2 * k)) /. (((x + h) + h) + (k * h)) by A2
.= ((cdif (f,h)) . (2 * k)) /. ((x + h) + (h + (k * h))) by RLVECT_1:def 3
.= ((cdif (f,h)) . (2 * k)) /. (x + (h + (h + (k * h)))) by RLVECT_1:def 3
.= ((cdif (f,h)) . (2 * k)) /. (x + ((h + h) + (k * h))) by RLVECT_1:def 3
.= ((cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h)) by BINOM:15, A31 ;
A4: ((fdif (f,h)) . (2 * k)) /. (x + h) = ((cdif (f,h)) . (2 * k)) /. ((x + h) + (k * h)) by A2
.= ((cdif (f,h)) . (2 * k)) /. ((x + (1 * h)) + (k * h)) by BINOM:13
.= ((cdif (f,h)) . (2 * k)) /. (x + ((1 * h) + (k * h))) by RLVECT_1:def 3
.= ((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)) by BINOM:15 ;
set r3 = ((cdif (f,h)) . (2 * k)) /. (x + (k * h));
set r2 = ((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h));
set r1 = ((cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h));
A5: (fdif (f,h)) . ((2 * k) + 1) is Function of V,W by Th2;
A6: (cdif (f,h)) . (2 * k) is Function of V,W by Th19;
A7: (cdif (f,h)) . ((2 * k) + 1) is Function of V,W by Th19;
A8: (fdif (f,h)) . (2 * k) is Function of V,W by Th2;
A9: ((cdif (f,h)) . ((2 * k) + 1)) /. ((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) = (cD (((cdif (f,h)) . (2 * k)),h)) /. ((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) by Def8
.= (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h))) - (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h))) by A6, Th5
.= (((cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) - ((((2 * (1. F)) ") * h) - (((2 * (1. F)) ") * h)))) - (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h))) by RLVECT_1:29
.= (((cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) - (0. V))) - (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h))) by RLVECT_1:15
.= (((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + (k * h))) by A35, RLVECT_1:13 ;
A10: ((cdif (f,h)) . ((2 * k) + 1)) /. ((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) = (cD (((cdif (f,h)) . (2 * k)),h)) /. ((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) by Def8
.= (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h))) - (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) - (((2 * (1. F)) ") * h))) by A6, Th5
.= (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h))) - (((cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) + ((((2 * (1. F)) ") * h) - (((2 * (1. F)) ") * h)))) by RLVECT_1:28
.= (((cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * (1. F)) ") * h)) + (((2 * (1. F)) ") * h))) - (((cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) + (0. V))) by RLVECT_1:15
.= (((cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) by A36, RLVECT_1:4 ;
A11: ((cdif (f,h)) . (2 * (k + 1))) /. (x + ((k + 1) * h)) = ((cdif (f,h)) . (((2 * k) + 1) + 1)) /. (x + ((k + 1) * h))
.= (cD (((cdif (f,h)) . ((2 * k) + 1)),h)) /. (x + ((k + 1) * h)) by Def8
.= ((((cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)))) - ((((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + (k * h)))) by A7, A10, A9, Th5 ;
((fdif (f,h)) . (2 * (k + 1))) /. x = ((fdif (f,h)) . (((2 * k) + 1) + 1)) /. x
.= (fD (((fdif (f,h)) . ((2 * k) + 1)),h)) /. x by Def6
.= (((fdif (f,h)) . ((2 * k) + 1)) /. (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) /. x) by A5, Th3
.= ((fD (((fdif (f,h)) . (2 * k)),h)) /. (x + h)) - (((fdif (f,h)) . ((2 * k) + 1)) /. x) by Def6
.= ((fD (((fdif (f,h)) . (2 * k)),h)) /. (x + h)) - ((fD (((fdif (f,h)) . (2 * k)),h)) /. x) by Def6
.= ((((fdif (f,h)) . (2 * k)) /. ((x + h) + h)) - (((fdif (f,h)) . (2 * k)) /. (x + h))) - ((fD (((fdif (f,h)) . (2 * k)),h)) /. x) by A8, Th3
.= ((((fdif (f,h)) . (2 * k)) /. ((x + h) + h)) - (((fdif (f,h)) . (2 * k)) /. (x + h))) - ((((fdif (f,h)) . (2 * k)) /. (x + h)) - (((fdif (f,h)) . (2 * k)) /. x)) by A8, Th3
.= ((((cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)))) - ((((cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) - (((cdif (f,h)) . (2 * k)) /. (x + (k * h)))) by A2, A3, A4 ;
hence ((fdif (f,h)) . (2 * (k + 1))) /. x = ((cdif (f,h)) . (2 * (k + 1))) /. (x + ((k + 1) * h)) by A11; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

let x be Element of V; :: thesis: ((fdif (f,h)) . (2 * 0)) /. x = ((cdif (f,h)) . (2 * 0)) /. (x + (0 * h))
((fdif (f,h)) . (2 * 0)) /. x = f /. x by Def6
.= ((cdif (f,h)) . (2 * 0)) /. x by Def8
.= ((cdif (f,h)) . (2 * 0)) /. (x + (0. V)) by RLVECT_1:4
.= ((cdif (f,h)) . (2 * 0)) /. (x + (0 * h)) by BINOM:12 ;
hence ((fdif (f,h)) . (2 * 0)) /. x = ((cdif (f,h)) . (2 * 0)) /. (x + (0 * h)) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A1);
hence ((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h)) ; :: thesis: verum