theorem Th25: :: PDIFF_1:25

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