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