:: deftheorem defines is_hpartial_differentiable`22_on PDIFF_3:def 13 :
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`22_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`22_in z ) ) );