theorem Th9: :: NDIFF10:9

for X, Y, Z being RealNormSpace
for f being PartFunc of Y,Z
for I being LinearOperator of X,Y
for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds
for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")