theorem Th37: :: LOPBAN14:36

for X, Y, Z being RealNormSpace
for I being Lipschitzian LinearOperator of Y,Z st I is one-to-one & I is onto & I is isometric holds
ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) )