let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for x being Point of S st I is isometric holds
I is_continuous_in x
let I be LinearOperator of S,T; :: thesis: for x being Point of S st I is isometric holds
I is_continuous_in x
let x0 be Point of S; :: thesis: ( I is isometric implies I is_continuous_in x0 )
assume AS1: I is isometric ; :: thesis: I is_continuous_in x0
P1: dom I = the carrier of S by FUNCT_2:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom I & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom I & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r ) ) )
assume P2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom I & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r ) )
take s = r; :: thesis: ( 0 < s & ( for x1 being Point of S st x1 in dom I & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r ) )
thus 0 < s by P2; :: thesis: for x1 being Point of S st x1 in dom I & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r
let x1 be Point of S; :: thesis: ( x1 in dom I & ||.(x1 - x0).|| < s implies ||.((I /. x1) - (I /. x0)).|| < r )
assume P3: ( x1 in dom I & ||.(x1 - x0).|| < s ) ; :: thesis: ||.((I /. x1) - (I /. x0)).|| < r
thus ||.((I /. x1) - (I /. x0)).|| < r by AS1, P3; :: thesis: verum

end;

hence I is_continuous_in x0 by NFCONT_1:7, P1; :: thesis: verum