let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_on Z
let I be LinearOperator of S,T; :: thesis: for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_on Z
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like implies I is_continuous_on Z )
assume A1: ( I is one-to-one & I is onto & I is isometric-like ) ; :: thesis: I is_continuous_on Z
A2: dom I = the carrier of S by FUNCT_2:def 1;
for x being Point of S st x in dom I holds
I | (dom I) is_continuous_in x by A1, Th32;
hence I is_continuous_on Z by A2, NFCONT_1:23, NFCONT_1:def 7; :: thesis: verum