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 st I . x in dom f holds
( f * I is_continuous_in x iff f is_continuous_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 st I . x in dom f holds
( f * I is_continuous_in x iff f is_continuous_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 st I . x in dom f holds
( f * I is_continuous_in x iff f is_continuous_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 st I . x in dom f holds
( f * I is_continuous_in x iff f is_continuous_in I . x )
set g = f * I;
let x be Point of S; :: thesis: ( I . x in dom f implies ( f * I is_continuous_in x iff f is_continuous_in I . x ) )
assume AS6: I . x in dom f ; :: thesis: ( f * I is_continuous_in x iff f is_continuous_in I . x )
P0: dom I = the carrier of S by FUNCT_2:def 1;

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

assume P1: f * I is_continuous_in x ; :: thesis: f is_continuous_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_continuous_in I . x by LM010, P2;
P3: J . (I . x) = x by AS2, P2, P0, FUNCT_1:34;
Q0: dom J = the carrier of T by FUNCT_2:def 1;
Q1: J . (I . x) in dom (f * I) by P1, P3, NFCONT_1:7;
Q3: (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 ;
( J . (I . x) = J /. (I . x) & I . x = I /. x ) ;
hence f is_continuous_in I . x by Q3, LM030, P3, P1, Q0, Q1, Q4; :: thesis: verum

end;

assume P2: f is_continuous_in I . x ; :: thesis: f * I is_continuous_in x
I . x = I /. x ;
hence f * I is_continuous_in x by P0, AS3, AS6, P2, LM010, LM030; :: thesis: verum