:: deftheorem defines is_partial_differentiable_in`1 NDIFF_7:def 4 :
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`1 z iff f * (reproj1 z) is_differentiable_in z `1 );