:: deftheorem defines is_partial_differentiable_on`2 NDIFF_7:def 9 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`2 z ) ) );