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_continuous_on X ; :: thesis:
then I " X c= I " (dom f) by NFCONT_1:def 7, RELAT_1:143;
then P3: I " X c= dom (f * I) by RELAT_1:147;
for x being Point of S st x in I " X holds
(f * I) | (I " X) is_continuous_in x

let x be Point of S; :: thesis:
assume x in I " X ; :: thesis:
then P5: ( x in dom I & I . x in X ) by FUNCT_1:def 7;
then P6: f | X is_continuous_in I . x by P2, NFCONT_1:def 7;
( X c= dom f & ( for y being Point of T st y in X holds
f | X is_continuous_in y ) ) by P2, NFCONT_1:def 7;
then I . x in (dom f) /\ X by P5, XBOOLE_0:def 4;
then I . x in dom (f | X) by RELAT_1:61;
then (f | X) * I is_continuous_in x by AS2, AS3, P6, LM040;
hence (f * I) | (I " X) is_continuous_in x by FX1; :: thesis:

end;

hence f * I is_continuous_on I " X by P3, NFCONT_1:def 7; :: thesis:

end;

assume P2: f * I is_continuous_on I " X ; :: thesis:
then ( I " X c= dom (f * I) & ( for x being Point of S st x in I " X holds
(f * I) | (I " X) is_continuous_in x ) ) by NFCONT_1:def 7;
then K1: I " X c= I " (dom f) by RELAT_1:147;
P3: X c= dom f by AS1, AS2, FUNCT_1:88, K1;
for y being Point of T st y in X holds
f | X is_continuous_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_continuous_in x by P2, NFCONT_1:def 7;
then P7: (f | X) * I is_continuous_in x by FX1;
I . x in dom (f | X) by P3, P4, P5, RELAT_1:57;
hence f | X is_continuous_in y by AS2, AS3, P5, P7, LM040; :: thesis:

end;

hence f is_continuous_on X by AS1, AS2, K1, FUNCT_1:88, NFCONT_1:def 7; :: thesis: