theorem LM020: :: NDIFF_7:9

for S, T being RealNormSpace
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
ex J being LinearOperator of T,S st
( J = I " & J is one-to-one & J is onto & J is isometric )