let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is isometric holds
I is_continuous_on Z
let I be LinearOperator of S,T; :: thesis: for Z being Subset of S st I is isometric holds
I is_continuous_on Z
let Z be Subset of S; :: thesis: ( I is isometric implies I is_continuous_on Z )
assume AS: I is isometric ; :: thesis: I is_continuous_on Z
P1: 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 AS, LM010;
hence I is_continuous_on Z by P1, NFCONT_1:23, NFCONT_1:def 7; :: thesis: verum