let f be PartFunc of REAL,REAL; :: thesis: for x0 being real number st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be real number ; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1: f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0
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 x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by Def5;

now

consider g being real number such that
A3: 0 < g and
A4: N = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;
x0 in REAL by XREAL_0:def 1;
then reconsider s2 = NAT --> x0 as Real_Sequence by FUNCOP_1:45;
let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
assume that
A5: rng s1 c= dom f and
A6: s1 is convergent and
A7: lim s1 = x0 and
A8: for n being Element of NAT holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f . x0 = lim (f /* s1) )
consider l being Element of NAT such that
A9: for m being Element of NAT st l <= m holds
abs ((s1 . m) - x0) < g by A6, A7, A3, SEQ_2:def 7;
reconsider c = s2 ^\ l as V8() Real_Sequence ;
deffunc H₁( Real) -> Element of REAL = (s1 . $1) - (s2 . $1);
consider s3 being Real_Sequence such that
A10: for n being Element of NAT holds s3 . n = H₁(n) from SEQ_1:sch 1();
A11: s3 = s1 - s2 by A10, RFUNCT_2:1;
then A12: s3 is convergent by A6, SEQ_2:11;
A13: rng c = {x0}

proof

thus rng c c= {x0} :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in {x0} )
assume y in rng c ; :: thesis: y in {x0}
then consider n being Element of NAT such that
A14: y = (s2 ^\ l) . n by FUNCT_2:113;
y = s2 . (n + l) by A14, NAT_1:def 3;
then y = x0 by FUNCOP_1:7;
hence y in {x0} by TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {x0} or y in rng c )
assume y in {x0} ; :: thesis: y in rng c
then A15: y = x0 by TARSKI:def 1;
c . 0 = s2 . (0 + l) by NAT_1:def 3
.= y by A15, FUNCOP_1:7 ;
hence y in rng c by VALUED_0:28; :: thesis: verum

end;

A16: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < p )
assume A17: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* c) . m) - (f . x0)) < p )
assume n <= m ; :: thesis: abs (((f /* c) . m) - (f . x0)) < p
x0 in N by RCOMP_1:16;
then rng c c= dom f by A2, A13, ZFMISC_1:31;
then abs (((f /* c) . m) - (f . x0)) = abs ((f . (c . m)) - (f . x0)) by FUNCT_2:108
.= abs ((f . (s2 . (m + l))) - (f . x0)) by NAT_1:def 3
.= abs ((f . x0) - (f . x0)) by FUNCOP_1:7
.= 0 by ABSVALUE:2 ;
hence abs (((f /* c) . m) - (f . x0)) < p by A17; :: thesis: verum

end;

then A18: f /* c is convergent by SEQ_2:def 6;
lim s2 = s2 . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
then lim s3 = x0 - x0 by A6, A7, A11, SEQ_2:12
.= 0 ;
then A19: lim (s3 ^\ l) = 0 by A12, SEQ_4:20;

A20: now

given n being Element of NAT such that A21: s3 . n = 0 ; :: thesis: contradiction
(s1 . n) - (s2 . n) = 0 by A10, A21;
hence contradiction by A8, FUNCOP_1:7; :: thesis: verum

end;

A22: now

given n being Element of NAT such that A23: (s3 ^\ l) . n = 0 ; :: thesis: contradiction
s3 . (n + l) = 0 by A23, NAT_1:def 3;
hence contradiction by A20; :: thesis: verum

end;

then s3 ^\ l is non-zero by SEQ_1:5;
then reconsider h = s3 ^\ l as convergent_to_0 Real_Sequence by A12, A19, Def1;

now

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

end;

then A24: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;

now

let n be Element of NAT ; :: thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A11, SEQM_3:15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1
.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum

end;

then A25: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A24, FUNCT_2:63
.= (f /* s1) ^\ l by A5, VALUED_0:27 ;
rng (h + c) c= N

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in N )
assume y in rng (h + c) ; :: thesis: y in N
then consider n being Element of NAT such that
A26: y = (h + c) . n by FUNCT_2:113;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A11, SEQM_3:15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by RFUNCT_2:1
.= s1 . (l + n) ;
then abs (((h + c) . n) - x0) < g by A9, NAT_1:12;
hence y in N by A4, A26, RCOMP_1:1; :: thesis: verum

end;

then A27: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A13, Th20;
then A28: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A12, A19, SEQ_2:15
.= 0 ;

now

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A29: h . n <> 0 by A22;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:8
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:8
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A29, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

end;

then A30: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
then A31: (f /* (h + c)) - (f /* c) is convergent by A12, A27, SEQ_2:14;
then A32: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A18, SEQ_2:5;
hence f /* s1 is convergent by A25, SEQ_4:21; :: thesis: f . x0 = lim (f /* s1)
lim (f /* c) = f . x0 by A16, A18, SEQ_2:def 7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by A28, A30, A31, A18, SEQ_2:6
.= f . x0 ;
hence f . x0 = lim (f /* s1) by A32, A25, SEQ_4:22; :: thesis: verum

end;

hence f is_continuous_in x0 by FCONT_1:2; :: thesis: verum