:: deftheorem defines `hpartial21| PDIFF_3:def 16 :
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`21_on Z holds
for b₃ being PartFunc of (REAL 2),REAL holds
( b₃ = f `hpartial21| Z iff ( dom b₃ = Z & ( for z being Element of REAL 2 st z in Z holds
b₃ . z = hpartdiff21 (f,z) ) ) );