let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_in x0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 implies ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 ) )
assume f is_differentiable_in x0 ; :: thesis: ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )
then consider N being Neighbourhood of x0 such that
N c= dom f and
A1: 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;
consider L being LINEAR, R being REST such that
A2: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1;
take R ; :: thesis: ( R . 0 = 0 & R is_continuous_in 0 )
consider p being Real such that
A3: for r being Real holds L . r = p * r by Def4;
(f . x0) - (f . x0) = (L . (x0 - x0)) + (R . (x0 - x0)) by A2, RCOMP_1:37;
then A4: 0 = (p * 0 ) + (R . 0 ) by A3;
hence R . 0 = 0 ; :: thesis: R is_continuous_in 0

A5: now

set s3 = cs;
let h be convergent_to_0 Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R . 0 )
A6: cs . 1 = 0 by FUNCOP_1:13;
(h " ) (#) (R /* h) is convergent by Def3;
then (h " ) (#) (R /* h) is bounded by SEQ_2:27;
then consider M being real number such that
M > 0 and
A7: for n being Element of NAT holds abs (((h " ) (#) (R /* h)) . n) < M by SEQ_2:15;
A8: h is convergent by Def1;
then A9: abs h is convergent by SEQ_4:26;
A10: h is non-zero by Def1;

A11: now

let n be Element of NAT ; :: thesis: ( cs . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )
abs (((h " ) (#) (R /* h)) . n) = abs (((h " ) . n) * ((R /* h) . n)) by SEQ_1:12
.= abs (((h . n) " ) * ((R /* h) . n)) by VALUED_1:10 ;
then A12: abs (((h . n) " ) * ((R /* h) . n)) <= M by A7;
0 <= abs ((R /* h) . n) by COMPLEX1:132;
then 0 <= (abs (R /* h)) . n by SEQ_1:16;
hence cs . n <= (abs (R /* h)) . n by FUNCOP_1:13; :: thesis: (abs (R /* h)) . n <= (M (#) (abs h)) . n
abs (h . n) >= 0 by COMPLEX1:132;
then (abs (h . n)) * (abs (((h . n) " ) * ((R /* h) . n))) <= M * (abs (h . n)) by A12, XREAL_1:66;
then abs ((h . n) * (((h . n) " ) * ((R /* h) . n))) <= M * (abs (h . n)) by COMPLEX1:151;
then A13: abs (((h . n) * ((h . n) " )) * ((R /* h) . n)) <= M * (abs (h . n)) ;
h . n <> 0 by A10, SEQ_1:7;
then abs (1 * ((R /* h) . n)) <= M * (abs (h . n)) by A13, XCMPLX_0:def 7;
then abs ((R /* h) . n) <= M * ((abs h) . n) by SEQ_1:16;
then abs ((R /* h) . n) <= (M (#) (abs h)) . n by SEQ_1:13;
hence (abs (R /* h)) . n <= (M (#) (abs h)) . n by SEQ_1:16; :: thesis: verum

end;

lim h = 0 by Def1;
then lim (abs h) = abs 0 by A8, SEQ_4:27
.= 0 by ABSVALUE:7 ;
then A14: lim (M (#) (abs h)) = M * 0 by A9, SEQ_2:22
.= lim cs by A6, SEQ_4:40 ;
A15: M (#) (abs h) is convergent by A9, SEQ_2:21;
then A16: abs (R /* h) is convergent by A14, A11, SEQ_2:33;
lim cs = 0 by A6, SEQ_4:40;
then lim (abs (R /* h)) = 0 by A15, A14, A11, SEQ_2:34;
hence ( R /* h is convergent & lim (R /* h) = R . 0 ) by A4, A16, SEQ_4:28; :: thesis: verum

end;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) implies ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) )
assume that
rng s1 c= dom R and
A17: ( s1 is convergent & lim s1 = 0 ) and
A18: for n being Element of NAT holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R . 0 )
s1 is non-zero by A18, SEQ_1:7;
then s1 is convergent_to_0 Real_Sequence by A17, Def1;
hence ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) by A5; :: thesis: verum

end;

hence R is_continuous_in 0 by FCONT_1:2; :: thesis: verum