:: deftheorem Def9 defines `| NDIFF_1:def 9 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for X being set st f is_differentiable_on X holds
for b<sub>5</sub> being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) holds
( b<sub>5</sub> = f `| X iff ( dom b₅ = X & ( for x being Point of S st x in X holds
b₅ /. x = diff (f,x) ) ) );