for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
for x being Point of S holds
( f * I is_differentiable_in x iff f is_differentiable_in I . x )