let S, T, W be RealNormSpace; :: thesis: 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 )
let f be PartFunc of T,W; :: thesis: 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 )
let I be LinearOperator of S,T; :: thesis: ( I is one-to-one & I is onto & I is isometric implies for x being Point of S holds
( f * I is_differentiable_in x iff f is_differentiable_in I . x ) )
assume that
AS2: ( I is one-to-one & I is onto ) and
AS3: I is isometric ; :: thesis: for x being Point of S holds
( f * I is_differentiable_in x iff f is_differentiable_in I . x )
P0: dom I = the carrier of S by FUNCT_2:def 1;
set g = f * I;
let x be Point of S; :: thesis: ( f * I is_differentiable_in x iff f is_differentiable_in I . x )

hereby :: thesis: ( f is_differentiable_in I . x implies f * I is_differentiable_in x )

assume P1: f * I is_differentiable_in x ; :: thesis: f is_differentiable_in I . x
consider J being LinearOperator of T,S such that
P2: ( J = I " & J is one-to-one & J is onto & J is isometric ) by LM020, AS2, AS3;
Q4: J is_differentiable_in I . x by LM090, P2;
P3: J . (I . x) = x by AS2, P2, P0, FUNCT_1:34;
(f * I) * J = f * (I * (I ")) by P2, RELAT_1:36
.= f * (id the carrier of T) by AS2, FUNCT_2:29
.= f by FUNCT_2:17 ;
hence f is_differentiable_in I . x by NDIFF_2:13, P3, P1, Q4; :: thesis: verum

end;

assume P2: f is_differentiable_in I . x ; :: thesis: f * I is_differentiable_in x
I is Lipschitzian LinearOperator of S,T by AS3;
then reconsider I0 = I as Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) by LOPBAN_1:def 9;
I0 = I ;
hence f * I is_differentiable_in x by P2, LM120, AS3; :: thesis: verum