theorem Th38: :: LOPBAN14:37

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 (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) )