:: deftheorem defines `partial| PDIFF_1:def 20 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f is_partial_differentiable_on X,i holds
for b<sub>6</sub> being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) holds
( b<sub>6</sub> = f `partial| (X,i) iff ( dom b₆ = X & ( for x being Point of (REAL-NS m) st x in X holds
b₆ /. x = partdiff (f,x,i) ) ) );