let F be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of F
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 constant 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 f be PartFunc of REAL, the carrier of F; :: 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 constant 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 constant 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 constant 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 constant 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 of F ex R being RestFunc of F 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 constant 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 constant 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;
reconsider z0 = 0 as Nat ;
( x0 + z0 < x0 + g & x0 - g < x0 - 0 ) by A9, XREAL_1:8, XREAL_1:15;
then A11: x0 in N2 by A10;

now :: thesis: for y being object st y in rng c holds
y in dom f

let y be object ; :: thesis: ( y in rng c implies 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;

then A12: rng c c= dom f ;
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;
reconsider z0 = 0 as Real ;
lim h = z0 ;
then lim (h + c) = z0 + 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;
for y being object st y in rng (c ^\ n) holds
y in N2 by A11, A15, TARSKI:def 1;
hence rng (c ^\ n) c= N2 ; :: thesis: rng ((h + c) ^\ n) c= N2

now :: thesis: for y being object st y in rng ((h + c) ^\ n) holds
y in N2

let y be object ; :: thesis: ( y in rng ((h + c) ^\ n) implies 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;
reconsider z0 = 0 as Nat ;
n + z0 <= 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;

hence rng ((h + c) ^\ n) c= N2 ; :: thesis: verum

end;

then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A19: rng ((h + c) ^\ n) c= N2 ;
consider L being LinearFunc of F, R being RestFunc of F such that
A20: for x being Real st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3;

now :: thesis: for y being object st y in rng (c ^\ n) holds
y in dom f

let y be object ; :: thesis: ( y in rng (c ^\ n) implies y in dom f )
assume A21: y in rng (c ^\ n) ; :: thesis: y in dom f
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A7, A21, TARSKI:def 1;
then y in N by A4, A11;
hence y in dom f by A2; :: thesis: verum

end;

then A22: rng (c ^\ n) c= dom f ;
A23: ( ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent & lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L /. 1 )

proof

deffunc H₁( Element of NAT ) -> Element of the carrier of F = (L . jj) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . $1);
consider s1 being sequence of the carrier of F such that
A24: for k being Element of NAT holds s1 . k = H₁(k) from FUNCT_2:sch 4();

A25: 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 /. jj)).|| < r

A26: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0. F ) by Def1;
let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st
for k being Nat st n1 <= k holds
||.((s1 . k) - (L /. jj)).|| < r )
assume 0 < r ; :: thesis: ex n1 being Nat st
for k being Nat st n1 <= k holds
||.((s1 . k) - (L /. jj)).|| < r
then consider m being Nat such that
A27: for k being Nat st m <= k holds
||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A26, NORMSP_1:def 7;
take n1 = m; :: thesis: for k being Nat st n1 <= k holds
||.((s1 . k) - (L /. jj)).|| < r
let k be Nat; :: thesis: ( n1 <= k implies ||.((s1 . k) - (L /. jj)).|| < r )
assume A28: n1 <= k ; :: thesis: ||.((s1 . k) - (L /. jj)).|| < r
A29: k in NAT by ORDINAL1:def 12;
A30: ||.((s1 . k) - (L /. jj)).|| = ||.(((L . jj) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . k)) - (L /. jj)).|| by A24, A29
.= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + ((L /. jj) - (L /. jj))).|| by RLVECT_1:28
.= ||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) + (0. F)).|| by RLVECT_1:15
.= ||.((((h ^\ n) ") (#) (R /* (h ^\ n))) . k).|| by RLVECT_1:4 ;
||.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - (0. F)).|| < r by A27, A28;
hence ||.((s1 . k) - (L /. jj)).|| < r by A30, RLVECT_1:13; :: thesis: verum

end;

consider s being Point of F such that
A31: for p1 being Real holds L /. p1 = p1 * s by Def2;
A32: L /. jj = 1 * s by A31
.= s by RLVECT_1:def 8 ;

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

let m be Element of NAT ; :: thesis: (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = s1 . m
A33: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) . m = ((((h ^\ n) ") (#) (L /* (h ^\ n))) + (((h ^\ n) ") (#) (R /* (h ^\ n)))) . m by NDIFF_1:9
.= ((((h ^\ n) ") (#) (L /* (h ^\ n))) . m) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NORMSP_1:def 2
.= ((((h ^\ n) ") . m) * ((L /* (h ^\ n)) . m)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by NDIFF_1:def 2
.= ((((h ^\ n) ") . m) * (L /. ((h ^\ n) . m))) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by FUNCT_2:115
.= ((((h ^\ n) ") . m) * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A31
.= ((((h ^\ n) . m) ") * (((h ^\ n) . m) * s)) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by VALUED_1:10
.= (((((h ^\ n) . m) ") * ((h ^\ n) . m)) * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def 7
.= (1 * s) + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by A33, XCMPLX_0:def 7
.= s + ((((h ^\ n) ") (#) (R /* (h ^\ n))) . m) by RLVECT_1:def 8
.= s1 . m by A24, A32 ; :: thesis: verum

end;

then A34: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = s1 by FUNCT_2:63;
hence ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) is convergent by A25, NORMSP_1:def 6; :: thesis: lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L /. 1
hence lim (((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n)))) = L /. 1 by A34, A25, NORMSP_1:def 7; :: thesis: verum

end;

for y being object st y in rng ((h + c) ^\ n) holds
y in dom f by A2, A4, A19;
then A35: rng ((h + c) ^\ n) c= dom f ;
for y being object st y in rng (h + c) holds
y in dom f by A2, A8;
then A36: rng (h + c) c= dom f ;
A37: 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 A38: ((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 A39: (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, A38, A39; :: thesis: verum

end;

A40: R is total by Def1;

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

let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
dom R = REAL by A40, FUNCT_2:def 1;
then A41: rng (h ^\ n) c= dom R ;
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def 3
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A35, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A22, FUNCT_2:109
.= (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A37
.= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A41, FUNCT_2:109
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def 2 ; :: thesis: verum

end;

then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A42: ((h ^\ n) ") (#) ((L /* (h ^\ n)) + (R /* (h ^\ n))) = ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) by A36, VALUED_0:27
.= ((h ^\ n) ") (#) (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) by A12, VALUED_0:27
.= ((h ^\ n) ") (#) (((f /* (h + c)) - (f /* c)) ^\ n) by NDIFF_1:16
.= ((h ") ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n) by SEQM_3:18
.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n by Th2 ;
then A43: L /. 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A23, LOPBAN_3:11;
thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A23, A42, LOPBAN_3:10; :: 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, A43, Def4; :: thesis: verum