for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )