theorem :: CFDIFF_1:16

for Y being Subset of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds
Y is open