theorem LM166: :: NDIFF_7:31

for W, X, Y being RealNormSpace
for f being PartFunc of [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")