for X being set
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z