let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let x0 be Real; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )

assume that

A1: f is_differentiable_in x0 and

A2: N c= dom f ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

consider N1 being Neighbourhood of x0 such that

N1 c= dom f and

A3: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1;

consider N2 being Neighbourhood of x0 such that

A4: N2 c= N and

A5: N2 c= N1 by RCOMP_1:17;

A6: N2 c= dom f by A2, A4;

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )

assume that

A7: rng c = {x0} and

A8: rng (h + c) c= N ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

consider g being Real such that

A9: 0 < g and

A10: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15;

then A11: x0 in N2 by A10;

A12: rng c c= dom f

( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

rng (c ^\ n) c= N2 and

A19: rng ((h + c) ^\ n) c= N2 ;

consider L being LinearFunc, R being RestFunc such that

A20: for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;

A21: rng (c ^\ n) c= dom f

A24: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )

A35: rng (h + c) c= dom f by A8, A2;

A36: for k being Element of NAT holds (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

then A40: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A35, VALUED_0:27

.= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ") by A12, VALUED_0:27

.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17

.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18

.= (((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;

then A41: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A24, SEQ_4:22;

thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, A40, SEQ_4:21; :: thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

for x being Real st x in N2 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A20, A5;

hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A41, Def5; :: thesis: verum

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let x0 be Real; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )

assume that

A1: f is_differentiable_in x0 and

A2: N c= dom f ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

consider N1 being Neighbourhood of x0 such that

N1 c= dom f and

A3: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1;

consider N2 being Neighbourhood of x0 such that

A4: N2 c= N and

A5: N2 c= N1 by RCOMP_1:17;

A6: N2 c= dom f by A2, A4;

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )

assume that

A7: rng c = {x0} and

A8: rng (h + c) c= N ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

consider g being Real such that

A9: 0 < g and

A10: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15;

then A11: x0 in N2 by A10;

A12: rng c c= dom f

proof

ex n being Element of NAT st
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )

assume y in rng c ; :: thesis: y in dom f

then y = x0 by A7, TARSKI:def 1;

then y in N by A4, A11;

hence y in dom f by A2; :: thesis: verum

end;assume y in rng c ; :: thesis: y in dom f

then y = x0 by A7, TARSKI:def 1;

then y in N by A4, A11;

hence y in dom f by A2; :: thesis: verum

( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

then consider n being Element of NAT such that
x0 in rng c
by A7, TARSKI:def 1;

then A13: lim c = x0 by SEQ_4:25;

lim h = 0 ;

then lim (h + c) = 0 + x0 by A13, SEQ_2:6

.= x0 ;

then consider n being Nat such that

A14: for m being Nat st n <= m holds

|.(((h + c) . m) - x0).| < g by A9, SEQ_2:def 7;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

A15: rng (c ^\ n) = {x0} by A7, VALUED_0:26;

thus rng (c ^\ n) c= N2 by A11, A15, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )

assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2

then consider m being Element of NAT such that

A16: y = ((h + c) ^\ n) . m by FUNCT_2:113;

n + 0 <= n + m by XREAL_1:7;

then A17: |.(((h + c) . (n + m)) - x0).| < g by A14;

then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;

then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def 3;

then A18: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;

- g < ((h + c) . (m + n)) - x0 by A17, SEQ_2:1;

then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def 3;

then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;

hence y in N2 by A10, A16, A18; :: thesis: verum

end;then A13: lim c = x0 by SEQ_4:25;

lim h = 0 ;

then lim (h + c) = 0 + x0 by A13, SEQ_2:6

.= x0 ;

then consider n being Nat such that

A14: for m being Nat st n <= m holds

|.(((h + c) . m) - x0).| < g by A9, SEQ_2:def 7;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

A15: rng (c ^\ n) = {x0} by A7, VALUED_0:26;

thus rng (c ^\ n) c= N2 by A11, A15, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )

assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2

then consider m being Element of NAT such that

A16: y = ((h + c) ^\ n) . m by FUNCT_2:113;

n + 0 <= n + m by XREAL_1:7;

then A17: |.(((h + c) . (n + m)) - x0).| < g by A14;

then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;

then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def 3;

then A18: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;

- g < ((h + c) . (m + n)) - x0 by A17, SEQ_2:1;

then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def 3;

then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;

hence y in N2 by A10, A16, A18; :: thesis: verum

rng (c ^\ n) c= N2 and

A19: rng ((h + c) ^\ n) c= N2 ;

consider L being LinearFunc, R being RestFunc such that

A20: for x being Real st x in N1 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;

A21: rng (c ^\ n) c= dom f

proof

A23:
L is total
by Def3;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )

assume A22: y in rng (c ^\ n) ; :: thesis: y in dom f

rng (c ^\ n) = rng c by VALUED_0:26;

then y = x0 by A7, A22, TARSKI:def 1;

then y in N by A4, A11;

hence y in dom f by A2; :: thesis: verum

end;assume A22: y in rng (c ^\ n) ; :: thesis: y in dom f

rng (c ^\ n) = rng c by VALUED_0:26;

then y = x0 by A7, A22, TARSKI:def 1;

then y in N by A4, A11;

hence y in dom f by A2; :: thesis: verum

A24: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )

proof

A34:
rng ((h + c) ^\ n) c= dom f
by A19, A4, A2;
deffunc H_{1}( Nat) -> set = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);

consider s1 being Real_Sequence such that

A25: for k being Nat holds s1 . k = H_{1}(k)
from SEQ_1:sch 1();

A30: for p1 being Real holds L . p1 = s * p1 by Def3;

A31: L . 1 = s * 1 by A30

.= s ;

hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A26, SEQ_2:def 6; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1

hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A33, A26, SEQ_2:def 7; :: thesis: verum

end;consider s1 being Real_Sequence such that

A25: for k being Nat holds s1 . k = H

A26: now :: thesis: for r being Real st 0 < r holds

ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

consider s being Real such that ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

A27:
( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 )
by Def2;

let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r )

assume 0 < r ; :: thesis: ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

then consider m being Nat such that

A28: for k being Nat st m <= k holds

|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| < r by A27, SEQ_2:def 7;

take n1 = m; :: thesis: for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

let k be Nat; :: thesis: ( n1 <= k implies |.((s1 . k) - (L . 1)).| < r )

assume A29: n1 <= k ; :: thesis: |.((s1 . k) - (L . 1)).| < r

|.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)).| by A25

.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| ;

hence |.((s1 . k) - (L . 1)).| < r by A28, A29; :: thesis: verum

end;let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r )

assume 0 < r ; :: thesis: ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

then consider m being Nat such that

A28: for k being Nat st m <= k holds

|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| < r by A27, SEQ_2:def 7;

take n1 = m; :: thesis: for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

let k be Nat; :: thesis: ( n1 <= k implies |.((s1 . k) - (L . 1)).| < r )

assume A29: n1 <= k ; :: thesis: |.((s1 . k) - (L . 1)).| < r

|.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)).| by A25

.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| ;

hence |.((s1 . k) - (L . 1)).| < r by A28, A29; :: thesis: verum

A30: for p1 being Real holds L . p1 = s * p1 by Def3;

A31: L . 1 = s * 1 by A30

.= s ;

now :: thesis: for m being Element of NAT holds (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m

then A33:
((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1
by FUNCT_2:63;let m be Element of NAT ; :: thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m

A32: (h ^\ n) . m <> 0 by SEQ_1:5;

thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10

.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A23, FUNCT_2:115

.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A30

.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)

.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32, XCMPLX_0:def 7

.= s1 . m by A25, A31 ; :: thesis: verum

end;A32: (h ^\ n) . m <> 0 by SEQ_1:5;

thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10

.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A23, FUNCT_2:115

.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A30

.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)

.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32, XCMPLX_0:def 7

.= s1 . m by A25, A31 ; :: thesis: verum

hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A26, SEQ_2:def 6; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1

hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A33, A26, SEQ_2:def 7; :: thesis: verum

A35: rng (h + c) c= dom f by A8, A2;

A36: for k being Element of NAT holds (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

proof

A39:
R is total
by Def2;
let k be Element of NAT ; :: thesis: (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;

then A37: ((h + c) ^\ n) . k in N2 by A19;

( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;

then A38: (c ^\ n) . k = x0 by A7, TARSKI:def 1;

(((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15

.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7

.= (h ^\ n) . k ;

hence (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A20, A5, A37, A38; :: thesis: verum

end;((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;

then A37: ((h + c) ^\ n) . k in N2 by A19;

( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;

then A38: (c ^\ n) . k = x0 by A7, TARSKI:def 1;

(((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15

.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7

.= (h ^\ n) . k ;

hence (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A20, A5, A37, A38; :: thesis: verum

now :: thesis: for k being Element of NAT holds ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k

then
(f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
by FUNCT_2:63;let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k

thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by RFUNCT_2:1

.= (f . (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A34, FUNCT_2:108

.= (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) by A21, FUNCT_2:108

.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A36

.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A23, FUNCT_2:115

.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A39, FUNCT_2:115

.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis: verum

end;thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by RFUNCT_2:1

.= (f . (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A34, FUNCT_2:108

.= (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) by A21, FUNCT_2:108

.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A36

.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A23, FUNCT_2:115

.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A39, FUNCT_2:115

.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis: verum

then A40: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A35, VALUED_0:27

.= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ") by A12, VALUED_0:27

.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17

.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18

.= (((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;

then A41: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A24, SEQ_4:22;

thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, A40, SEQ_4:21; :: thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

for x being Real st x in N2 holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A20, A5;

hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A41, Def5; :: thesis: verum