:: deftheorem defines partdiff`1 NDIFF_7:def 6 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds partdiff`1 (f,z) = diff ((f * (reproj1 z)),(z `1));