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
A1: ( N c= dom f & 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, Th9;
then A4: 0c = (a * 0c ) + (R /. 0c ) by A3;
hence R /. 0c = 0c ; :: thesis: R is_continuous_in 0c

A6: 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
A7: ( M > 0 & ( for n being Element of NAT holds |.(((h " ) (#) (R /* h)) . n).| < M ) ) by COMSEQ_2:8;
A8: ( h is non-zero & h is convergent & lim h = 0 ) by Def1;
A10: lim |.h.| = |.0 .| by A8, COMSEQ_2:11;
A11: M (#) |.h.| is convergent by SEQ_2:21;
A12: lim (M (#) |.h.|) = M * |.0 .| by A10, SEQ_2:22
.= M * 0 by ABSVALUE:7
.= 0 ;

A13: 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
A14: for n being Element of NAT st m <= n holds
abs (((M (#) |.h.|) . n) - 0 ) < p by A11, A12, 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 A15: m <= n ; :: thesis: |.(((R /* h) . n) - 0c ).| < p
A16: h . n <> 0c by COMSEQ_1:4;
|.(((h " ) (#) (R /* h)) . n).| = |.(((h " ) . n) * ((R /* h) . n)).| by VALUED_1:5
.= |.(((h . n) " ) * ((R /* h) . n)).| by VALUED_1:10 ;
then A17: |.(((h . n) " ) * ((R /* h) . n)).| <= M by A7;
|.(h . n).| >= 0 by COMPLEX1:132;
then |.(h . n).| * |.(((h . n) " ) * ((R /* h) . n)).| <= M * |.(h . n).| by A17, XREAL_1:66;
then |.((h . n) * (((h . n) " ) * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:151;
then |.(((h . n) * ((h . n) " )) * ((R /* h) . n)).| <= M * |.(h . n).| ;
then |.(1r * ((R /* h) . n)).| <= M * |.(h . n).| by A16, XCMPLX_0:def 7;
then |.((R /* h) . n).| <= M * (|.h.| . n) by VALUED_1:18;
then A18: |.((R /* h) . n).| <= (M (#) |.h.|) . n by SEQ_1:13;
A19: abs (((M (#) |.h.|) . n) - 0 ) < p by A14, A15;
0 <= (M (#) |.h.|) . n by A18, COMPLEX1:132;
then (M (#) |.h.|) . n < p by A19, ABSVALUE:def 1;
hence |.(((R /* h) . n) - 0c ).| < p by XXREAL_0:2, A18; :: 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, A13, COMSEQ_2:def 5; :: thesis: verum

end;

A20: 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 A21: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) ) ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. 0c )
then s1 is non-zero by COMSEQ_1:4;
then s1 is convergent_to_0 Complex_Sequence by A21, Def1;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) by A6; :: thesis: verum

end;

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