let S, T, W be RealNormSpace; :: thesis: 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 )
let f be PartFunc of T,W; :: thesis: 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 )
let I be LinearOperator of S,T; :: thesis: 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 )
let X be set ; :: thesis: ( X c= the carrier of T & I is one-to-one & I is onto & I is isometric implies ( f is_differentiable_on X iff f * I is_differentiable_on I " X ) )
assume that
AS1: X c= the carrier of T and
AS2: ( I is one-to-one & I is onto ) and
AS3: I is isometric ; :: thesis: ( f is_differentiable_on X iff f * I is_differentiable_on I " X )

hereby :: thesis: ( f * I is_differentiable_on I " X implies f is_differentiable_on X )

assume P2: f is_differentiable_on X ; :: thesis: f * I is_differentiable_on I " X
P3: I " X c= I " (dom f) by P2, RELAT_1:143;
for x being Point of S st x in I " X holds
(f * I) | (I " X) is_differentiable_in x

proof

let x be Point of S; :: thesis: ( x in I " X implies (f * I) | (I " X) is_differentiable_in x )
assume x in I " X ; :: thesis: (f * I) | (I " X) is_differentiable_in x
then ( x in dom I & I . x in X ) by FUNCT_1:def 7;
then P6: f | X is_differentiable_in I . x by P2;
(f | X) * I is_differentiable_in x by AS2, AS3, P6, LM150;
hence (f * I) | (I " X) is_differentiable_in x by FX1; :: thesis: verum

end;

hence f * I is_differentiable_on I " X by P3, RELAT_1:147; :: thesis: verum

end;

assume P2: f * I is_differentiable_on I " X ; :: thesis: f is_differentiable_on X
then K1: I " X c= I " (dom f) by RELAT_1:147;
for y being Point of T st y in X holds
f | X is_differentiable_in y

proof

let y be Point of T; :: thesis: ( y in X implies f | X is_differentiable_in y )
assume P4: y in X ; :: thesis: f | X is_differentiable_in y
consider x being Point of S such that
P5: y = I . x by AS2, FUNCT_2:113;
dom I = the carrier of S by FUNCT_2:def 1;
then x in I " X by P4, P5, FUNCT_1:def 7;
then (f * I) | (I " X) is_differentiable_in x by P2;
then (f | X) * I is_differentiable_in x by FX1;
hence f | X is_differentiable_in y by AS2, AS3, P5, LM150; :: thesis: verum

end;

hence f is_differentiable_on X by AS1, AS2, K1, FUNCT_1:88; :: thesis: verum