for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st Z is open holds
( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`1 x ) ) )