let f be PartFunc of REAL,REAL; :: thesis: for x0 being real number
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 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 number ; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 LINEAR ex R being REST st
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def5;
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, XBOOLE_1:1;
let h be convergent_to_0 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 number 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

let y be set ; :: 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;

ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

x0 in rng c by A7, TARSKI:def 1;
then A13: lim c = x0 by SEQ_4:25;
A14: h is convergent by Def1;
then A15: h + c is convergent by SEQ_2:5;
lim h = 0 by Def1;
then lim (h + c) = 0 + x0 by A13, A14, SEQ_2:6
.= x0 ;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < g by A9, A15, SEQ_2:def 7;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A17: rng (c ^\ n) = {x0} by A7, VALUED_0:26;
thus rng (c ^\ n) c= N2 :: thesis: rng ((h + c) ^\ n) c= N2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; :: thesis: y in N2
hence y in N2 by A11, A17, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: 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
A18: y = ((h + c) ^\ n) . m by FUNCT_2:113;
n + 0 <= n + m by XREAL_1:7;
then A19: abs (((h + c) . (n + m)) - x0) < g by A16;
then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;
then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def 3;
then A20: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;
- g < ((h + c) . (m + n)) - x0 by A19, 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, A18, A20; :: thesis: verum

end;

then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A21: rng ((h + c) ^\ n) c= N2 ;
consider L being LINEAR, R being REST such that
A22: for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
A23: rng (c ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )
assume A24: y in rng (c ^\ n) ; :: thesis: y in dom f
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A7, A24, TARSKI:def 1;
then y in N by A4, A11;
hence y in dom f by A2; :: thesis: verum

end;

A25: L is total by Def4;
A26: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )

proof

deffunc H₁( Element of NAT ) -> Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A27: for k being Element of NAT holds s1 . k = H₁(k) from SEQ_1:sch 1();

A28: now

A29: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by Def3;
let r be real number ; :: thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r )
assume 0 < r ; :: thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
then consider m being Element of NAT such that
A30: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A29, SEQ_2:def 7;
take n1 = m; :: thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
let k be Element of NAT ; :: thesis: ( n1 <= k implies abs ((s1 . k) - (L . 1)) < r )
assume A31: n1 <= k ; :: thesis: abs ((s1 . k) - (L . 1)) < r
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)) by A27
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence abs ((s1 . k) - (L . 1)) < r by A30, A31; :: thesis: verum

end;

consider s being Real such that
A32: for p1 being Real holds L . p1 = s * p1 by Def4;
A33: L . 1 = s * 1 by A32
.= s ;

now

let m be Element of NAT ; :: thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
h ^\ n is non-zero by Def1;
then A34: (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 A25, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A34, XCMPLX_0:def 7
.= s1 . m by A27, A33 ; :: thesis: verum

end;

then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A28, 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 A35, A28, SEQ_2:def 7; :: thesis: verum

end;

A36: rng ((h + c) ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in dom f
then y in N2 by A21;
then y in N by A4;
hence y in dom f by A2; :: thesis: verum

end;

A37: rng (h + c) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; :: thesis: y in dom f
then y in N by A8;
hence y in dom f by A2; :: thesis: verum

end;

A38: 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

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 A39: ((h + c) ^\ n) . k in N2 by A21;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;
then A40: (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 A22, A5, A39, A40; :: thesis: verum

end;

A41: R is total by Def3;

now

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 A36, FUNCT_2:108
.= (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) by A23, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A38
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A25, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A41, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis: verum

end;

then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A42: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A37, 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 A43: L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A26, SEQ_4:22;
thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A26, A42, 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 A22, A5;
hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A43, Def6; :: thesis: verum