:: deftheorem defines is_differentiable_on CFDIFF_1:def 9 :
for f being PartFunc of COMPLEX,COMPLEX
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & f | X is differentiable ) );