:: deftheorem Def91 defines `partial`1| NDIFF_7:def 10 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
for b<sub>6</sub> being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) holds
( b<sub>6</sub> = f `partial`1| Z iff ( dom b<sub>6</sub> = Z & ( for z being Point of [:X,Y:] st z in Z holds
b<sub>6</sub> /. z = partdiff`1 (f,z) ) ) );