let x0 be Complex; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st f is_differentiable_in x0 holds
ex R being C_REST st
( R /. 0c = 0c & R is_continuous_in 0c )
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is_differentiable_in x0 implies ex R being C_REST st
( R /. 0c = 0c & R is_continuous_in 0c ) )
assume f is_differentiable_in x0 ; :: thesis: ex R being C_REST st
( R /. 0c = 0c & R is_continuous_in 0c )
then consider N being Neighbourhood of x0 such that
N c= dom f and
A1: ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
consider L being C_LINEAR, R being C_REST such that
A2: for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1;
take R ; :: thesis: ( R /. 0c = 0c & R is_continuous_in 0c )
consider a being Complex such that
A3: for z being Complex holds L /. z = a * z by Def4;
(f /. x0) - (f /. x0) = (L /. (x0 - x0)) + (R /. (x0 - x0)) by A2, Th7;
then A4: 0c = (a * 0c ) + (R /. 0c ) by A3;
hence R /. 0c = 0c ; :: thesis: R is_continuous_in 0c

A5: now

let h be convergent_to_0 Complex_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R /. 0c )
(h " ) (#) (R /* h) is bounded by Def3;
then consider M being Real such that
M > 0 and
A6: for n being Element of NAT holds |.(((h " ) (#) (R /* h)) . n).| < M by COMSEQ_2:8;
A7: M (#) |.h.| is convergent by SEQ_2:21;
lim h = 0 by Def1;
then lim |.h.| = |.0 .| by COMSEQ_2:11;
then A8: lim (M (#) |.h.|) = M * |.0 .| by SEQ_2:22
.= M * 0 by ABSVALUE:7
.= 0 ;

A9: now

let p be Real; :: thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c ).| < p )
assume 0 < p ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c ).| < p
then consider m being Element of NAT such that
A10: for n being Element of NAT st m <= n holds
abs (((M (#) |.h.|) . n) - 0 ) < p by A7, A8, SEQ_2:def 7;
take m = m; :: thesis: for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c ).| < p

now

let n be Element of NAT ; :: thesis: ( m <= n implies |.(((R /* h) . n) - 0c ).| < p )
assume m <= n ; :: thesis: |.(((R /* h) . n) - 0c ).| < p
then A11: abs (((M (#) |.h.|) . n) - 0 ) < p by A10;
|.(((h " ) (#) (R /* h)) . n).| = |.(((h " ) . n) * ((R /* h) . n)).| by VALUED_1:5
.= |.(((h . n) " ) * ((R /* h) . n)).| by VALUED_1:10 ;
then A12: |.(((h . n) " ) * ((R /* h) . n)).| <= M by A6;
|.(h . n).| >= 0 by COMPLEX1:132;
then |.(h . n).| * |.(((h . n) " ) * ((R /* h) . n)).| <= M * |.(h . n).| by A12, XREAL_1:66;
then |.((h . n) * (((h . n) " ) * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:151;
then ( h . n <> 0c & |.(((h . n) * ((h . n) " )) * ((R /* h) . n)).| <= M * |.(h . n).| ) by COMSEQ_1:4;
then |.(1r * ((R /* h) . n)).| <= M * |.(h . n).| by XCMPLX_0:def 7;
then |.((R /* h) . n).| <= M * (|.h.| . n) by VALUED_1:18;
then A13: |.((R /* h) . n).| <= (M (#) |.h.|) . n by SEQ_1:13;
then 0 <= (M (#) |.h.|) . n by COMPLEX1:132;
then (M (#) |.h.|) . n < p by A11, ABSVALUE:def 1;
hence |.(((R /* h) . n) - 0c ).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

hence for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c ).| < p ; :: thesis: verum

end;

hence R /* h is convergent by COMSEQ_2:def 4; :: thesis: lim (R /* h) = R /. 0c
hence lim (R /* h) = R /. 0c by A4, A9, COMSEQ_2:def 5; :: thesis: verum

end;

A14: now

let s1 be Complex_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 /. 0c ) )
assume that
rng s1 c= dom R and
A15: ( s1 is convergent & lim s1 = 0 ) and
A16: for n being Element of NAT holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. 0c )
s1 is non-empty by A16, COMSEQ_1:4;
then s1 is convergent_to_0 Complex_Sequence by A15, Def1;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) by A5; :: thesis: verum

end;

dom R = COMPLEX by PARTFUN1:def 4;
hence R is_continuous_in 0c by A14, CFCONT_1:53; :: thesis: verum