let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
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 & 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant 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 constant 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));
lim (- h) = - (lim h) by SEQ_2:10;
then A5: - h is 0 -convergent ;
A6: lim (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))) = diff (f,x0) by A1, A2, A4, Th12, A5;
set fp = (h ") (#) ((f /* (h + c)) - (f /* c));
A7: diff (f,x0) = diff (f,x0) ;
then A8: ((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)) is convergent by A1, A2, A4, Th12, A5;
A9: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A3, A7, Th12;
then A10: ((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))) is convergent by A8;

A11: now :: thesis: for n being Element of NAT holds (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c))) . n = ((f /* (c + h)) - (f /* (c - h))) . n

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:7
.= (((f /* (c + h)) - (f /* (c - h))) . n) + (((f /* c) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((f /* (c + h)) - (f /* (c - h))) . n ; :: thesis: verum

end;

A12: (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:47
.= (2 ") (#) (((h ") (#) ((f /* (c + h)) - (f /* c))) + ((- 1) (#) ((h ") (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:18
.= (2 ") (#) (((h ") (#) ((f /* (c + h)) - (f /* c))) + ((h ") (#) ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:19
.= (2 ") (#) ((h ") (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:16
.= ((2 ") (#) (h ")) (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))) by SEQ_1:18
.= ((2 (#) h) ") (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))) by SEQ_1:46
.= ((2 (#) h) ") (#) ((f /* (c + h)) - ((f /* c) - (- ((f /* (c + (- h))) - (f /* c))))) by SEQ_1:30
.= ((2 (#) h) ") (#) ((f /* (c + h)) - ((f /* (c + (- h))) - ((f /* c) - (f /* c)))) by SEQ_1:30
.= ((2 (#) h) ") (#) (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c))) by SEQ_1:30 ;
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 A9, A8, A6, SEQ_2:6
.= 2 * (diff (f,x0)) ;
then A13: lim ((2 ") (#) (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))))) = (2 ") * (2 * (diff (f,x0))) by A10, SEQ_2:8
.= diff (f,x0) ;
(2 ") (#) (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)))) is convergent by A10;
hence ( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) ) by A13, A12, A11, FUNCT_2:63; :: thesis: verum