theorem :: CFDIFF_1:17

for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Complex st rng f = {a1} holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )