theorem Th32: :: REAL_NS3:31

for S, T being RealNormSpace
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