:: deftheorem defines is_hpartial_differentiable`23_on PDIFF_5:def 24 :
for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_hpartial_differentiable`23_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_hpartial_differentiable`23_in u ) ) );