let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_in x0 holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 implies for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 ) )
assume A1: f is_differentiable_in x0 ; :: 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 & rng ((- h) + c) c= dom f holds
( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 )
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 & rng ((- h) + c) c= dom f holds
( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 )
let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f implies ( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 ) )
assume that
A2: rng c = {x0} and
A3: rng (h + c) c= dom f and
A4: rng ((- h) + c) c= dom f ; :: thesis: ( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 )
set fm = ((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c));
A5: lim (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))) = diff f,x0 by A1, A2, A4, Th12;
set fp = (h " ) (#) ((f /* (h + c)) - (f /* c));
A6: diff f,x0 = diff f,x0 ;
then A7: ((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)) is convergent by A1, A2, A4, Th12;
A8: (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A3, A6, Th12;
then A9: ((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))) is convergent by A7, SEQ_2:19;

A10: now

let n be Element of NAT ; :: thesis: (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c))) . n = ((f /* (c + h)) - (f /* (c - h))) . n
thus (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c))) . n = (((f /* (c + h)) - (f /* (c - h))) . n) + (((f /* c) - (f /* c)) . n) by SEQ_1:11
.= (((f /* (c + h)) - (f /* (c - h))) . n) + (((f /* c) . n) - ((f /* c) . n)) by RFUNCT_2:6
.= ((f /* (c + h)) - (f /* (c - h))) . n ; :: thesis: verum

end;

A11: (2 " ) (#) (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)))) = (2 " ) (#) (((h " ) (#) ((f /* (c + h)) - (f /* c))) + (((- 1) (#) (h " )) (#) ((f /* (c + (- h))) - (f /* c)))) by SEQ_1:55
.= (2 " ) (#) (((h " ) (#) ((f /* (c + h)) - (f /* c))) + ((- 1) (#) ((h " ) (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:26
.= (2 " ) (#) (((h " ) (#) ((f /* (c + h)) - (f /* c))) + ((h " ) (#) ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:27
.= (2 " ) (#) ((h " ) (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:24
.= ((2 " ) (#) (h " )) (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))) by SEQ_1:26
.= ((2 (#) h) " ) (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))) by SEQ_1:54
.= ((2 (#) h) " ) (#) ((f /* (c + h)) - ((f /* c) - (- ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:38
.= ((2 (#) h) " ) (#) ((f /* (c + h)) - ((f /* (c + (- h))) - ((f /* c) - (f /* c)))) by SEQ_1:38
.= ((2 (#) h) " ) (#) (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c))) by SEQ_1:38 ;
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = diff f,x0 by A1, A2, A3, Th12;
then lim (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)))) = (1 * (diff f,x0)) + (diff f,x0) by A8, A7, A5, SEQ_2:20
.= 2 * (diff f,x0) ;
then A12: lim ((2 " ) (#) (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))))) = (2 " ) * (2 * (diff f,x0)) by A9, SEQ_2:22
.= diff f,x0 ;
(2 " ) (#) (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)))) is convergent by A9, SEQ_2:21;
hence ( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 ) by A12, A11, A10, FUNCT_2:113; :: thesis: verum