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