:: deftheorem defines is_partial_differentiable_in`2 NDIFF_7:def 5 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_in`2 z iff f * (reproj2 z) is_differentiable_in z `2 );