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_continuous_on X iff f * I is_continuous_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_continuous_on X iff f * I is_continuous_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_continuous_on X iff f * I is_continuous_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_continuous_on X iff f * I is_continuous_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_continuous_on X iff f * I is_continuous_on I " X )

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

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

proof

let x be Point of S; :: thesis: ( x in I " X implies (f * I) | (I " X) is_continuous_in x )
assume x in I " X ; :: thesis: (f * I) | (I " X) is_continuous_in x
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: verum

end;

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

end;

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

proof

let y be Point of T; :: thesis: ( y in X implies f | X is_continuous_in y )
assume P4: y in X ; :: thesis: f | X is_continuous_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_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: verum

end;

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