theorem :: CFDIFF_1:27

for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 1r ) )