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