theorem :: REAL_NS3:30

for V, W being RealNormSpace
for L being LinearOperator of V,W st L is one-to-one & L is onto & L is isometric-like holds
L is_continuous_on the carrier of V by Th30, LOPBAN_7:6;