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