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
A1: Z c= dom f and
A2: f | Z = id Z ; :: thesis: ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 1r ) )
reconsider L = id COMPLEX as PartFunc of COMPLEX ,COMPLEX ;
P0: COMPLEX c= COMPLEX ;
for b being Complex holds L /. b = 1r * b by PARTFUN2:12, P0;
then reconsider L = L as C_LINEAR by Def4;
set R = cf;
A3: dom cf = COMPLEX by FUNCOP_1:19;

now

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

A4: now

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

end;

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

end;

then reconsider R = cf as C_REST by Def3;

A7: now

let x be Complex; :: thesis: ( x in Z implies f /. x = x )
assume A8: x in Z ; :: thesis: f /. x = x
then (f | Z) . x = x by A2, FUNCT_1:35;
then f . x = x by A8, FUNCT_1:72;
hence f /. x = x by A1, A8, PARTFUN1:def 8; :: thesis: verum

end;

A9: now

let x0 be Complex; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= Z by Th12;
A12: N c= dom f by A1, A11, XBOOLE_1:1;
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)) )
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = x - (f /. x0) by A7, A11
.= x - x0 by A7, A10
.= (L /. (x - x0)) + 0c by PARTFUN2:12, P0
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A12, Def6; :: thesis: verum

end;

hence A13: f is_differentiable_on Z by A1, Th18; :: 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 A15: f is_differentiable_in x0 by A9;
then ex N being Neighbourhood of x0 st
( 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;
then consider N being Neighbourhood of x0 such that
A16: N c= dom f ;
consider N1 being Neighbourhood of x0 such that
A17: N1 c= Z by A14, Th12;
consider N2 being Neighbourhood of x0 such that
A18: ( N2 c= N1 & N2 c= N ) by Th10;
A19: N2 c= dom f by A16, A18, XBOOLE_1:1;
A20: 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)) )
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 A7, A17
.= x - x0 by A7, A14
.= (L /. (x - x0)) + 0c by PARTFUN2:12, P0
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

thus (f `| Z) /. x0 = diff f,x0 by A13, A14, Def12
.= L /. 1r by A15, A19, A20, Def7
.= 1r by PARTFUN2:12, P0 ; :: thesis: verum