reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;
set R = cf;
reconsider L = id COMPLEX as PartFunc of COMPLEX,COMPLEX ;
A1: COMPLEX c= COMPLEX ;
for b being Complex holds L /. b = 1r * b

proof

let b be Complex; :: thesis: L /. b = 1r * b
b in COMPLEX by XCMPLX_0:def 2;
hence L /. b = 1r * b by A1, PARTFUN2:6; :: thesis: verum

end;

then reconsider L = L as C_LinearFunc by Def4;

now :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )

let h be non-zero 0 -convergent Complex_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )

now :: thesis: for n being Nat holds ((h ") (#) (cf /* h)) . n = 0c

let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0c
A3: ( n in NAT & rng h c= dom cf ) by ORDINAL1:def 12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A3, FUNCT_2:109
.= ((h ") . n) * 0c
.= 0c ; :: thesis: verum

end;

then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def 18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; :: thesis: verum

end;

then reconsider R = cf as C_RestFunc by Def3;
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 1r ) )
let Z be open Subset of COMPLEX; :: thesis: ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 1r ) ) )
assume that
A4: Z c= dom f and
A5: f | Z = id Z ; :: thesis: ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 1r ) )

A6: now :: thesis: for x being Complex st x in Z holds
f /. x = x

let x be Complex; :: thesis: ( x in Z implies f /. x = x )
assume A7: x in Z ; :: thesis: f /. x = x
then (f | Z) . x = x by A5, FUNCT_1:18;
then f . x = x by A7, FUNCT_1:49;
hence f /. x = x by A4, A7, PARTFUN1:def 6; :: thesis: verum

end;

A8: now :: thesis: for x0 being Complex st x0 in Z holds
f is_differentiable_in x0

let x0 be Complex; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A9: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A10: N c= Z by Th9;
A11: for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))

proof

let x be Complex; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A12: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A10
.= x - x0 by A6, A9
.= (L /. (x - x0)) + 0c by A1, PARTFUN2:6, A12
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A12 ;
:: thesis: verum

end;

N c= dom f by A4, A10;
hence f is_differentiable_in x0 by A11; :: thesis: verum

end;

hence A13: f is_differentiable_on Z by A4, Th15; :: thesis: for x being Complex st x in Z holds
(f `| Z) /. x = 1r
let x0 be Complex; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 1r )
assume A14: x0 in Z ; :: thesis: (f `| Z) /. x0 = 1r
then consider N1 being Neighbourhood of x0 such that
A15: N1 c= Z by Th9;
A16: f is_differentiable_in x0 by A8, A14;
then ex N being Neighbourhood of x0 st
( N c= dom f & 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)) ) ;
then consider N being Neighbourhood of x0 such that
A17: N c= dom f ;
consider N2 being Neighbourhood of x0 such that
A18: N2 c= N1 and
A19: N2 c= N by Lm1;
A20: N2 c= dom f by A17, A19;
A21: for x being Complex st x in N2 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))

proof

let x be Complex; :: thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A22: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N2 ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then x in N1 by A18;
hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A15
.= x - x0 by A6, A14
.= (L /. (x - x0)) + 0c by A1, PARTFUN2:6, A22
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A22 ;
:: thesis: verum

end;

thus (f `| Z) /. x0 = diff (f,x0) by A13, A14, Def12
.= L /. 1r by A16, A20, A21, Def7
.= 1r ; :: thesis: verum