let x0 be Complex; :: thesis:
let f be PartFunc of COMPLEX,COMPLEX; :: thesis:
assume f is_differentiable_in x0 ; :: thesis:
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:
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:

let h be non-zero 0 -convergent Complex_Sequence; :: thesis:
(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 ;

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
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:

let n be Nat; :: thesis:
assume m <= n ; :: thesis:
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:

end;

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

end;

end;

end;