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 ; :: 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 )
A3: f | Z is differentiable by A1;
assume A4: x0 in Z ; :: thesis: f is_differentiable_in x0
then x0 in dom (f | Z) by A2, RELAT_1:57;
then f | Z is_differentiable_in x0 by A3;
then consider N being Neighbourhood of x0 such that
A5: N c= dom (f | Z) and
A6: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
take N ; :: according to CFDIFF_1:def 6 :: thesis: ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc 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:61;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A5; :: thesis: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Complex st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LinearFunc, R being C_RestFunc such that
A7: for x being Complex st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A6;
take L ; :: thesis: ex R being C_RestFunc 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 A8: 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 A7;
then A9: (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A8, PARTFUN2:15;
x0 in (dom f) /\ Z by A2, A4, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9, PARTFUN2:16; :: thesis: verum

end;

assume that
A10: Z c= dom f and
A11: for x being Complex st x in Z holds
f is_differentiable_in x ; :: thesis: f is_differentiable_on Z
thus Z c= dom f by A10; :: 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 A12: x0 in Z by RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by Th9;
f is_differentiable_in x0 by A11, A12;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: 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 N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Lm1;
A18: N2 c= Z by A13, A16;
take N2 ; :: according to CFDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
N2 c= dom f by A14, A17;
then N2 c= (dom f) /\ Z by A18, XBOOLE_1:19;
hence A19: N2 c= dom (f | Z) by RELAT_1:61; :: thesis: ex L being C_LinearFunc ex R being C_RestFunc 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_LinearFunc, R being C_RestFunc such that
A20: for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A15;
A21: x0 in N2 by Th7;
take L ; :: thesis: ex R being C_RestFunc 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 A22: 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 A17, A20;
then ((f | Z) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:15;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A21, PARTFUN2:15; :: thesis: verum