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 A2: ( rng c = {x0} & rng (h + c) c= dom f & 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 fp = (h " ) (#) ((f /* (h + c)) - (f /* c));
set fm = ((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c));
A3: diff f,x0 = diff f,x0 ;
then A4: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = diff f,x0 ) by A1, A2, Th12;
A5: ( ((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)) is convergent & lim (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))) = diff f,x0 ) by A1, A2, A3, Th12;
then A6: ((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))) is convergent by A4, SEQ_2:19;
then A7: (2 " ) (#) (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)))) is convergent by SEQ_2:21;
lim (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c)))) = (1 * (diff f,x0)) + (diff f,x0) by A4, A5, SEQ_2:20
.= 2 * (diff f,x0) ;
then A8: lim ((2 " ) (#) (((h " ) (#) ((f /* (h + c)) - (f /* c))) + (((- h) " ) (#) ((f /* ((- h) + c)) - (f /* c))))) = (2 " ) * (2 * (diff f,x0)) by A6, SEQ_2:22
.= diff f,x0 ;
A9: (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 ;

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;

hence ( ((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f /* (c + h)) - (f /* (c - h)))) = diff f,x0 ) by A7, A8, A9, FUNCT_2:113; :: thesis: verum