for X being set
for f being PartFunc of REAL,REAL st ( for x being set st x in X holds
f . x <> 0 ) & f is_differentiable_on X holds
f ^ is_differentiable_on X