let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )
thus ( f is_differentiable_in x0 implies ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) ) :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) implies f is_differentiable_in x0 )

proof

assume A1: f is_differentiable_in x0 ; :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) )
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L being LinearFunc ex R being RestFunc st
for g being Real st g in N holds
(f . g) - (f . x0) = (L . (g - x0)) + (R . (g - x0)) ;
thus ex N being Neighbourhood of x0 st N c= dom f by A2; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent )
assume that
A3: rng c = {x0} and
A4: rng (h + c) c= dom f ; :: thesis: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
A5: lim h = 0 ;
consider r being Real such that
A6: 0 < r and
A7: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
consider k being Nat such that
A8: for n being Nat st k <= n holds
|.((h . n) - 0).| < r by A5, A6, SEQ_2:def 7;
set h1 = h ^\ k;
rng ((h ^\ k) + c) c= N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((h ^\ k) + c) or x in N )
assume x in rng ((h ^\ k) + c) ; :: thesis: x in N
then consider n being Element of NAT such that
A9: x = ((h ^\ k) + c) . n by FUNCT_2:113;
c . n in rng c by VALUED_0:28;
then c . n = x0 by A3, TARSKI:def 1;
then A10: x = ((h ^\ k) . n) + x0 by A9, SEQ_1:7
.= (h . (n + k)) + x0 by NAT_1:def 3 ;
|.((h . (n + k)) - 0).| < r by A8, NAT_1:12;
then h . (n + k) in ].(0 - r),(0 + r).[ by RCOMP_1:1;
then h . (n + k) in { g where g is Real : ( - r < g & g < r ) } by RCOMP_1:def 2;
then A11: ex g being Real st
( g = h . (n + k) & - r < g & g < r ) ;
then A12: (h . (n + k)) + x0 < x0 + r by XREAL_1:6;
x0 + (- r) < (h . (n + k)) + x0 by A11, XREAL_1:6;
then (h . (n + k)) + x0 in { g where g is Real : ( x0 - r < g & g < x0 + r ) } by A12;
hence x in N by A7, A10, RCOMP_1:def 2; :: thesis: verum

end;

then A13: ((h ^\ k) ") (#) ((f /* ((h ^\ k) + c)) - (f /* c)) is convergent by A1, A2, A3, FDIFF_1:12;
A14: {x0} c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in dom f )
assume x in {x0} ; :: thesis: x in dom f
then A15: x = x0 by TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in dom f by A2, A15; :: thesis: verum

end;

c ^\ k = c by VALUED_0:26;
then ((h ^\ k) ") (#) ((f /* ((h ^\ k) + c)) - (f /* c)) = ((h ^\ k) ") (#) ((f /* ((h + c) ^\ k)) - (f /* (c ^\ k))) by SEQM_3:15
.= ((h ^\ k) ") (#) (((f /* (h + c)) ^\ k) - (f /* (c ^\ k))) by A4, VALUED_0:27
.= ((h ^\ k) ") (#) (((f /* (h + c)) ^\ k) - ((f /* c) ^\ k)) by A3, A14, VALUED_0:27
.= ((h ^\ k) ") (#) (((f /* (h + c)) - (f /* c)) ^\ k) by SEQM_3:17
.= ((h ") ^\ k) (#) (((f /* (h + c)) - (f /* c)) ^\ k) by SEQM_3:18
.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ k by SEQM_3:19 ;
hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A13, SEQ_4:21; :: thesis: verum

end;

assume that
A16: ex N being Neighbourhood of x0 st N c= dom f and
A17: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ; :: thesis: f is_differentiable_in x0
thus f is_differentiable_in x0 by A16, A17, Lm1; :: thesis: verum