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 r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

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 r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let W be VectSp of G; :: thesis: for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let f be Function of V,W; :: thesis: for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let x, h be Element of V; :: thesis: for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let r be Element of G; :: thesis: for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let n be Nat; :: thesis: ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

defpred S_{1}[ Nat] means for x being Element of V holds ((fdif ((r (#) f),h)) . ($1 + 1)) /. x = r * (((fdif (f,h)) . ($1 + 1)) /. x);

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 ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x) ; :: thesis: verum

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

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 r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let W be VectSp of G; :: thesis: for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let f be Function of V,W; :: thesis: for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let x, h be Element of V; :: thesis: for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let r be Element of G; :: thesis: for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

let n be Nat; :: thesis: ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

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 ((r (#) f),h)) . (k + 1)) /. x = r * (((fdif (f,h)) . (k + 1)) /. x) ; :: thesis: S_{1}[k + 1]

let x be Element of V; :: thesis: ((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = r * (((fdif (f,h)) . ((k + 1) + 1)) /. x)

A3: ( ((fdif ((r (#) f),h)) . (k + 1)) /. x = r * (((fdif (f,h)) . (k + 1)) /. x) & ((fdif ((r (#) f),h)) . (k + 1)) /. (x + h) = r * (((fdif (f,h)) . (k + 1)) /. (x + h)) ) by A2;

reconsider rfdk = (fdif ((r (#) f),h)) . (k + 1) as Function of V,W by Th2;

reconsider fdk = (fdif (f,h)) . (k + 1) as Function of V,W by Th2;

((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = (fD (((fdif ((r (#) f),h)) . (k + 1)),h)) /. x by Def6

.= (rfdk /. (x + h)) - (rfdk /. x) by Th3

.= r * ((fdk /. (x + h)) - (fdk /. x)) by VECTSP_1:23, A3

.= r * ((fD (fdk,h)) /. x) by Th3

.= r * (((fdif (f,h)) . ((k + 1) + 1)) /. x) by Def6 ;

hence ((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = r * (((fdif (f,h)) . ((k + 1) + 1)) /. x) ; :: thesis: verum

end;assume A2: for x being Element of V holds ((fdif ((r (#) f),h)) . (k + 1)) /. x = r * (((fdif (f,h)) . (k + 1)) /. x) ; :: thesis: S

let x be Element of V; :: thesis: ((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = r * (((fdif (f,h)) . ((k + 1) + 1)) /. x)

A3: ( ((fdif ((r (#) f),h)) . (k + 1)) /. x = r * (((fdif (f,h)) . (k + 1)) /. x) & ((fdif ((r (#) f),h)) . (k + 1)) /. (x + h) = r * (((fdif (f,h)) . (k + 1)) /. (x + h)) ) by A2;

reconsider rfdk = (fdif ((r (#) f),h)) . (k + 1) as Function of V,W by Th2;

reconsider fdk = (fdif (f,h)) . (k + 1) as Function of V,W by Th2;

((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = (fD (((fdif ((r (#) f),h)) . (k + 1)),h)) /. x by Def6

.= (rfdk /. (x + h)) - (rfdk /. x) by Th3

.= r * ((fdk /. (x + h)) - (fdk /. x)) by VECTSP_1:23, A3

.= r * ((fD (fdk,h)) /. x) by Th3

.= r * (((fdif (f,h)) . ((k + 1) + 1)) /. x) by Def6 ;

hence ((fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x = r * (((fdif (f,h)) . ((k + 1) + 1)) /. x) ; :: thesis: verum

proof

for n being Nat holds S
let x be Element of V; :: thesis: ((fdif ((r (#) f),h)) . (0 + 1)) /. x = r * (((fdif (f,h)) . (0 + 1)) /. x)

x in the carrier of V ;

then A7: x in dom (r (#) f) by FUNCT_2:def 1;

x + h in the carrier of V ;

then A8: x + h in dom (r (#) f) by FUNCT_2:def 1;

((fdif ((r (#) f),h)) . (0 + 1)) /. x = (fD (((fdif ((r (#) f),h)) . 0),h)) /. x by Def6

.= (fD ((r (#) f),h)) /. x by Def6

.= ((r (#) f) /. (x + h)) - ((r (#) f) /. x) by Th3

.= (r * (f /. (x + h))) - ((r (#) f) /. x) by A8, Def4X

.= (r * (f /. (x + h))) - (r * (f /. x)) by A7, Def4X

.= r * ((f /. (x + h)) - (f /. x)) by VECTSP_1:23

.= r * ((fD (f,h)) /. x) by Th3

.= r * ((fD (((fdif (f,h)) . 0),h)) /. x) by Def6

.= r * (((fdif (f,h)) . (0 + 1)) /. x) by Def6 ;

hence ((fdif ((r (#) f),h)) . (0 + 1)) /. x = r * (((fdif (f,h)) . (0 + 1)) /. x) ; :: thesis: verum

end;x in the carrier of V ;

then A7: x in dom (r (#) f) by FUNCT_2:def 1;

x + h in the carrier of V ;

then A8: x + h in dom (r (#) f) by FUNCT_2:def 1;

((fdif ((r (#) f),h)) . (0 + 1)) /. x = (fD (((fdif ((r (#) f),h)) . 0),h)) /. x by Def6

.= (fD ((r (#) f),h)) /. x by Def6

.= ((r (#) f) /. (x + h)) - ((r (#) f) /. x) by Th3

.= (r * (f /. (x + h))) - ((r (#) f) /. x) by A8, Def4X

.= (r * (f /. (x + h))) - (r * (f /. x)) by A7, Def4X

.= r * ((f /. (x + h)) - (f /. x)) by VECTSP_1:23

.= r * ((fD (f,h)) /. x) by Th3

.= r * ((fD (((fdif (f,h)) . 0),h)) /. x) by Def6

.= r * (((fdif (f,h)) . (0 + 1)) /. x) by Def6 ;

hence ((fdif ((r (#) f),h)) . (0 + 1)) /. x = r * (((fdif (f,h)) . (0 + 1)) /. x) ; :: thesis: verum

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