:: deftheorem defines differentiable CFDIFF_1:def 8 :
for f being PartFunc of COMPLEX,COMPLEX holds
( f is differentiable iff for x being Complex st x in dom f holds
f is_differentiable_in x );