theorem Th30: :: REAL_NS3:29

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 Lipschitzian ;