theorem :: NDIFF_7:30

for W, X, Y being RealNormSpace
for f being PartFunc of (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*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)) ")