theorem :: PDIFF_6:31

for X being set
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m) by XBOOLE_1:1;