theorem :: LOPBAN14:39

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