:: deftheorem defines is_partial_differentiable_on PDIFF_1:def 19 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f | X is_partial_differentiable_in x,i ) ) );