:: deftheorem Def6 defines `partial| PDIFF_9:def 6 :
for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,i holds
for b<sub>5</sub> being PartFunc of (REAL m),REAL holds
( b<sub>5</sub> = f `partial| (Z,i) iff ( dom b₅ = Z & ( for x being Element of REAL m st x in Z holds
b₅ /. x = partdiff (f,x,i) ) ) );