theorem :: PDIFF_6:33

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )