theorem LM400: :: NDIFF_7:41

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))