let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for x being Point of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_in x
let I be LinearOperator of S,T; :: thesis: for x being Point of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_in x
let x be Point of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like implies I is_continuous_in x )
assume ( I is one-to-one & I is onto & I is isometric-like ) ; :: thesis: I is_continuous_in x
then I is_continuous_on the carrier of S by Th30, LOPBAN_7:6;
hence I is_continuous_in x ; :: thesis: verum