:: deftheorem Def92 defines `partial`2| NDIFF_7:def 11 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds
for b<sub>6</sub> being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) holds
( b<sub>6</sub> = f `partial`2| 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`2 (f,z) ) ) );