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