for X, Y, Z being RealNormSpace
for V being Subset of Y
for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )