:: deftheorem defines `hpartial11| PDIFF_5:def 28 :
for f being PartFunc of (REAL 3),REAL
for D being set st f is_hpartial_differentiable`11_on D holds
for b₃ being PartFunc of (REAL 3),REAL holds
( b₃ = f `hpartial11| D iff ( dom b₃ = D & ( for u being Element of REAL 3 st u in D holds
b₃ . u = hpartdiff11 (f,u) ) ) );