theorem LM015: :: NDIFF_7:8

for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is isometric holds
I is_continuous_on Z