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