for n being non zero Element of NAT
for Y being Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open