theorem Th15: :: CFDIFF_1:15

for f being PartFunc of COMPLEX,COMPLEX
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 ) ) )