let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )
let Z be open Subset of COMPLEX ; :: thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) ) )
set R = cf;
A1: 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 )

now

let n be Nat; :: thesis: ((h " ) (#) (cf /* h)) . n = 0c
A2: ( n in NAT & rng h c= dom cf ) by A1, ORDINAL1:def 13;
thus ((h " ) (#) (cf /* h)) . n = ((h " ) . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h " ) . n) * (cf /. (h . n)) by A2, FUNCT_2:186
.= ((h " ) . n) * 0c by FUNCOP_1:13
.= 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:48, CFCONT_1:49; :: thesis: verum

end;

then reconsider R = cf as C_REST by Def3;
set L = cf;
for x being Complex holds cf /. x = 0c * x by FUNCOP_1:13;
then reconsider L = cf as C_LINEAR by Def4;
assume that
A3: Z c= dom f and
A4: f | Z is constant ; :: thesis: ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )
consider a1 being Complex such that
A5: for x being Complex st x in Z /\ (dom f) holds
f /. x = a1 by A4, PARTFUN2:54;

A6: now

let x0 be Complex; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A7: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: N c= dom f by A3, A8, XBOOLE_1:1;
A10: x0 in Z /\ (dom f) by A3, A7, XBOOLE_0:def 4;
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))
then x in Z /\ (dom f) by A8, A9, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5
.= a1 - a1 by A5, A10
.= (L /. (x - x0)) + 0c by FUNCOP_1:13
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

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

end;

hence A11: f is_differentiable_on Z by A3, Th15; :: thesis: for x being Complex st x in Z holds
(f `| Z) /. x = 0c
let x0 be Complex; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c )
assume A12: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0c
then consider N being Neighbourhood of x0 such that
A13: N c= Z by Th9;
A14: N c= dom f by A3, A13, XBOOLE_1:1;
A15: x0 in Z /\ (dom f) by A3, A12, XBOOLE_0:def 4;
A16: 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))
then x in Z /\ (dom f) by A13, A14, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5
.= a1 - a1 by A5, A15
.= (L /. (x - x0)) + 0c by FUNCOP_1:13
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

A17: f is_differentiable_in x0 by A6, A12;
thus (f `| Z) /. x0 = diff f,x0 by A11, A12, Def12
.= L /. 1r by A17, A14, A16, Def7
.= 0c by FUNCOP_1:13 ; :: thesis: verum