let S, T, W be RealNormSpace; 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; 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; ( 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
; 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; ( 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
; ( 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 ( f is_continuous_in I . x implies f * I is_continuous_in x )
assume P1:
f * I is_continuous_in x
;
f is_continuous_in I . xconsider 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;
verum
end;
assume P2:
f is_continuous_in I . x
; f * I is_continuous_in x
I . x = I /. x
;
hence
f * I is_continuous_in x
by P0, AS3, AS6, P2, LM010, LM030; verum