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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A6, A1);

hence ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h)) ; :: thesis: verum

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

A1: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[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_{1}[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;assume A2: for x being Element of V holds ((fdif (f,h)) . k) /. x = ((bdif (f,h)) . k) /. (x + (k * h)) ; :: thesis: S

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

proof

for n being Nat holds S
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;((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

hence ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h)) ; :: thesis: verum