for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 ) by PDIFF_2:9;