:: deftheorem defines `partial1| PDIFF_2:def 4 :
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_partial_differentiable`1_on Z holds
for b₃ being PartFunc of (REAL 2),REAL holds
( b₃ = f `partial1| Z iff ( dom b₃ = Z & ( for z being Element of REAL 2 st z in Z holds
b₃ . z = partdiff (f,z,1) ) ) );