theorem Th29: :: REAL_NS3:28

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
ex K being LinearOperator of W,V st
( K = L " & K is one-to-one & K is onto & K is isometric-like )