let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for Z being open Subset of COMPLEX holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) ) )
let Z be open Subset of COMPLEX ; :: thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) ) )
thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) ) ) :: thesis: ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )

proof

assume A1: f is_differentiable_on Z ; :: thesis: ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) )
hence A2: Z c= dom f by Def9; :: thesis: for x being Complex st x in Z holds
f is_differentiable_in x
let x0 be Complex; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A3: x0 in Z ; :: thesis: f is_differentiable_in x0
then AA: x0 in dom (f | Z) by A2, RELAT_1:86;
f | Z is differentiable by A1, Def9;
then f | Z is_differentiable_in x0 by AA, Def8;
then consider N being Neighbourhood of x0 such that
A4: ( N c= dom (f | Z) & ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6;
take N ; :: according to CFDIFF_1:def 6 :: thesis: ( N c= dom f & ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
dom (f | Z) = (dom f) /\ Z by RELAT_1:90;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A4, XBOOLE_1:1; :: thesis: ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
A5: x0 in (dom f) /\ Z by A2, A3, XBOOLE_0:def 4;
consider L being C_LINEAR, R being C_REST such that
A6: for x being Complex st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A4;
take L ; :: thesis: ex R being C_REST st
for z being Complex st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; :: thesis: for z being Complex st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Complex; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A7: x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A6;
then (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A4, A7, PARTFUN2:32;
hence (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, PARTFUN2:34; :: thesis: verum

end;

assume A8: ( Z c= dom f & ( for x being Complex st x in Z holds
f is_differentiable_in x ) ) ; :: thesis: f is_differentiable_on Z
hence Z c= dom f ; :: according to CFDIFF_1:def 9 :: thesis: f | Z is differentiable
let x0 be Complex; :: according to CFDIFF_1:def 8 :: thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 )
assume x0 in dom (f | Z) ; :: thesis: f | Z is_differentiable_in x0
then A9: ( x0 in dom f & x0 in Z ) by RELAT_1:86;
then f is_differentiable_in x0 by A8;
then consider N being Neighbourhood of x0 such that
A10: ( 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;
consider N1 being Neighbourhood of x0 such that
A11: N1 c= Z by A9, Th12;
consider N2 being Neighbourhood of x0 such that
A12: ( N2 c= N1 & N2 c= N ) by Th10;
take N2 ; :: according to CFDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
A13: N2 c= dom f by A10, A12, XBOOLE_1:1;
N2 c= Z by A11, A12, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A13, XBOOLE_1:19;
hence A14: N2 c= dom (f | Z) by RELAT_1:90; :: thesis: ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LINEAR, R being C_REST such that
A15: for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A10;
take L ; :: thesis: ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; :: thesis: for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Complex; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A16: x in N2 ; :: thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A12, A15;
then A17: ((f | Z) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A14, A16, PARTFUN2:32;
x0 in N2 by Th9;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A14, A17, PARTFUN2:32; :: thesis: verum