:: deftheorem defines is_partial_differentiable`2_on PDIFF_4:def 2 :
for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,2 ) ) );