let x0 be Complex; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds
ex R being C_RestFunc 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_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c ) )
assume f is_differentiable_in x0 ; :: thesis: ex R being C_RestFunc 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_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
consider L being C_LinearFunc, R being C_RestFunc 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 :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( R /* h is convergent & lim (R /* h) = R /. 0c )

let h be non-zero 0 -convergent 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 Nat holds |.(((h ") (#) (R /* h)) . n).| < M by COMSEQ_2:8;
lim h = 0 by Def1;
then lim |.h.| = |.0.| by SEQ_2:27;
then A7: lim (M (#) |.h.|) = M * |.0.| by SEQ_2:8
.= M * 0 by ABSVALUE:2
.= 0 ;

A8: now :: thesis: for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((R /* h) . n) - 0c).| < p

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

now :: thesis: for n being Nat st m <= n holds
|.(((R /* h) . n) - 0c).| < p

let n be Nat; :: thesis: ( m <= n implies |.(((R /* h) . n) - 0c).| < p )
assume m <= n ; :: thesis: |.(((R /* h) . n) - 0c).| < p
then A10: |.(((M (#) |.h.|) . n) - 0).| < p by A9;
|.(((h ") (#) (R /* h)) . n).| = |.(((h ") . n) * ((R /* h) . n)).| by VALUED_1:5
.= |.(((h . n) ") * ((R /* h) . n)).| by VALUED_1:10 ;
then A11: |.(((h . n) ") * ((R /* h) . n)).| <= M by A6;
A12: n in NAT by ORDINAL1:def 12;
|.(h . n).| >= 0 by COMPLEX1:46;
then |.(h . n).| * |.(((h . n) ") * ((R /* h) . n)).| <= M * |.(h . n).| by A11, XREAL_1:64;
then |.((h . n) * (((h . n) ") * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:65;
then ( h . n <> 0c & |.(((h . n) * ((h . n) ")) * ((R /* h) . n)).| <= M * |.(h . n).| ) by COMSEQ_1:4, A12;
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:9;
0 <= |.((R /* h) . n).| by COMPLEX1:46;
then 0 <= (M (#) |.h.|) . n by A13;
then (M (#) |.h.|) . n < p by A10, ABSVALUE:def 1;
hence |.(((R /* h) . n) - 0c).| < p by A13, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

end;

A14: now :: thesis: for s1 being Complex_Sequence st rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Nat holds s1 . n <> 0 ) holds
( R /* s1 is convergent & lim (R /* s1) = R /. 0c )

let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being 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 Nat holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. 0c )
for n being Element of NAT holds s1 . n <> 0 by A16;
then s1 is non-zero by COMSEQ_1:4;
then s1 is non-zero 0 -convergent 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 2;
hence R is_continuous_in 0c by A14, CFCONT_1:31; :: thesis: verum