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 holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . 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 holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . 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 holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))
let f be Function of V,W; :: thesis: for x, h being Element of V
for n being Nat holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))
let x, h be Element of V; :: thesis: for n being Nat holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))
let n be Nat; :: thesis: ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))
defpred S₁[ Nat] means for x being Element of V holds ((fdif (f,h)) . $1) /. x = ((bdif (f,h)) . $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)) . k) /. x = ((bdif (f,h)) . k) /. (x + (k * h)) ; :: thesis: S₁[k + 1]
let x be Element of V; :: thesis: ((fdif (f,h)) . (k + 1)) /. x = ((bdif (f,h)) . (k + 1)) /. (x + ((k + 1) * h))
A3: ((fdif (f,h)) . k) /. (x + h) = ((bdif (f,h)) . k) /. ((x + h) + (k * h)) by A2;
reconsider fdk = (fdif (f,h)) . k as Function of the carrier of V, the carrier of W by Th2;
N2: (k * h) + h = (k * h) + (1 * h) by BINOM:13
.= (k + 1) * h by BINOM:15 ;
N3: k * h = (k * h) + (0. V) by RLVECT_1:4
.= (k * h) + (h - h) by RLVECT_1:15
.= ((k + 1) * h) - h by N2, RLVECT_1:28 ;
A5: (bdif (f,h)) . k is Function of the carrier of V, the carrier of W by Th12;
((fdif (f,h)) . (k + 1)) /. x = (fD (fdk,h)) /. x by Def6
.= (fdk /. (x + h)) - (fdk /. x) by Th3
.= (((bdif (f,h)) . k) /. ((x + h) + (k * h))) - (((bdif (f,h)) . k) /. (x + (k * h))) by A2, A3
.= (((bdif (f,h)) . k) /. (x + (h + (k * h)))) - (((bdif (f,h)) . k) /. (x + (k * h))) by RLVECT_1:def 3
.= (((bdif (f,h)) . k) /. (x + ((k + 1) * h))) - (((bdif (f,h)) . k) /. ((x + ((k + 1) * h)) - h)) by RLVECT_1:28, N3, N2
.= (bD (((bdif (f,h)) . k),h)) /. (x + ((k + 1) * h)) by A5, Th4
.= ((bdif (f,h)) . (k + 1)) /. (x + ((k + 1) * h)) by Def7 ;
hence ((fdif (f,h)) . (k + 1)) /. x = ((bdif (f,h)) . (k + 1)) /. (x + ((k + 1) * h)) ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

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

end;

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