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