let S, T, W be RealNormSpace; :: thesis:
let f be PartFunc of T,W; :: thesis:
let I be LinearOperator of S,T; :: thesis:
let X be set ; :: thesis:
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:

hereby :: thesis:

assume P2: f is_differentiable_on X ; :: thesis:
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

let x be Point of S; :: thesis:
assume x in I " X ; :: thesis:
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:

end;

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

end;

assume P2: f * I is_differentiable_on I " X ; :: thesis:
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

let y be Point of T; :: thesis:
assume P4: y in X ; :: thesis:
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:

end;

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