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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 LINEAR ex R being REST st
for g being Real st g in N holds
(f . g) - (f . x0) = (L . (g - x0)) + (R . (g - x0)) by FDIFF_1:def 5;
thus ex N being Neighbourhood of x0 st N c= dom f by A2; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent
let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent )
assume A3: ( rng c = {x0} & rng (h + c) c= dom f ) ; :: thesis: (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent
A4: ( h is convergent & lim h = 0 & h is non-zero ) by FDIFF_1:def 1;
consider r being real number such that
A5: ( 0 < r & N = ].(x0 - r),(x0 + r).[ ) by RCOMP_1:def 7;
consider k being Element of NAT such that
A6: for n being Element of NAT st k <= n holds
abs ((h . n) - 0 ) < r by A4, A5, SEQ_2:def 7;
set h1 = h ^\ k;
rng ((h ^\ k) + c) c= N

proof

let x be set ; :: 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
A7: x = ((h ^\ k) + c) . n by FUNCT_2:190;
c . n in rng c by VALUED_0:28;
then c . n = x0 by A3, TARSKI:def 1;
then A8: x = ((h ^\ k) . n) + x0 by A7, SEQ_1:11
.= (h . (n + k)) + x0 by NAT_1:def 3 ;
abs ((h . (n + k)) - 0 ) < r by A6, NAT_1:12;
then h . (n + k) in ].(0 - r),(0 + r).[ by RCOMP_1:8;
then h . (n + k) in { g where g is Real : ( - r < g & g < r ) } by RCOMP_1:def 2;
then A9: ex g being Real st
( g = h . (n + k) & - r < g & g < r ) ;
then A10: x0 + (- r) < (h . (n + k)) + x0 by XREAL_1:8;
(h . (n + k)) + x0 < x0 + r by A9, XREAL_1:8;
then (h . (n + k)) + x0 in { g where g is Real : ( x0 - r < g & g < x0 + r ) } by A10;
hence x in N by A5, A8, RCOMP_1:def 2; :: thesis: verum

end;

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

proof

let x be set ; :: 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 A13: x = x0 by TARSKI:def 1;
x0 in N by RCOMP_1:37;
hence x in dom f by A2, A13; :: 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:37
.= ((h ^\ k) " ) (#) (((f /* (h + c)) ^\ k) - (f /* (c ^\ k))) by A3, VALUED_0:27
.= ((h ^\ k) " ) (#) (((f /* (h + c)) ^\ k) - ((f /* c) ^\ k)) by A3, A12, VALUED_0:27
.= ((h ^\ k) " ) (#) (((f /* (h + c)) - (f /* c)) ^\ k) by SEQM_3:39
.= ((h " ) ^\ k) (#) (((f /* (h + c)) - (f /* c)) ^\ k) by SEQM_3:41
.= ((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ k by SEQM_3:42 ;
hence (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A11, SEQ_4:35; :: thesis: verum

end;

assume ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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
hence f is_differentiable_in x0 by Lm1; :: thesis: verum