for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T
for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds
( f is_differentiable_on X iff f * I is_differentiable_on I " X )