theorem LM210: :: NDIFF_7:35

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) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )