let S, T be RealNormSpace; :: thesis:
let I be LinearOperator of S,T; :: thesis:
let x0 be Point of S; :: thesis:
assume AS1: I is isometric ; :: thesis:
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:
assume P2: 0 < r ; :: thesis:
take s = r; :: thesis:
thus 0 < s by P2; :: thesis:
let x1 be Point of S; :: thesis:
assume P3: ( x1 in dom I & ||.(x1 - x0).|| < s ) ; :: thesis:
thus ||.((I /. x1) - (I /. x0)).|| < r by AS1, P3; :: thesis:

end;

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