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