:: deftheorem Def9 defines `partial| NDIFF_5:def 9 :
for G being RealNormSpace-Sequence
for S being RealNormSpace
for i being set
for f being PartFunc of (product G),S
for X being set st f is_partial_differentiable_on X,i holds
for b<sub>6</sub> being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) holds
( b<sub>6</sub> = f `partial| (X,i) iff ( dom b₆ = X & ( for x being Point of (product G) st x in X holds
b₆ /. x = partdiff (f,x,i) ) ) );