theorem Th22: :: PDIFF_5:22
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds
( f is_hpartial_differentiable`21_in u iff pdiff1 (f,2) is_partial_differentiable_in u,1 ) by PDIFF_4:13;