let X, Y, Z, W be RealNormSpace; :: thesis: 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 ")) ) )
let I be Lipschitzian LinearOperator of X,Z; :: thesis: 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 ")) ) )
let J be Lipschitzian LinearOperator of Y,W; :: thesis: ( I is one-to-one & I is onto & I is isometric & J is one-to-one & J is onto & J is isometric implies 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 ")) ) ) )
assume A1: ( I is one-to-one & I is onto & I is isometric & J is one-to-one & J is onto & J is isometric ) ; :: thesis: 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 ")) ) )
consider H being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Z,Y)) such that
A2: ( H is one-to-one & H is onto & H is isometric & ( for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds H . x = x * (I ") ) ) by A1, Th38;
consider L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Z,Y)),(R_NormSpace_of_BoundedLinearOperators (Z,W)) such that
A3: ( L is one-to-one & L is onto & L is isometric & ( for x being Point of (R_NormSpace_of_BoundedLinearOperators (Z,Y)) holds L . x = J * x ) ) by A1, Th37;
reconsider K = L * H as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Z,W)) by LOPBAN_2:2;
take K ; :: thesis: ( 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 ")) ) )
thus ( K is one-to-one & K is onto ) by A2, A3, FUNCT_2:27; :: thesis: ( K is isometric & ( for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds K . x = J * (x * (I ")) ) )
for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.(K . x).|| = ||.x.||

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ||.(K . x).|| = ||.x.||
thus ||.(K . x).|| = ||.(L . (H . x)).|| by FUNCT_2:15
.= ||.(H . x).|| by NDIFF_7:7, A3
.= ||.x.|| by A2, NDIFF_7:7 ; :: thesis: verum

end;

hence K is isometric by NDIFF_7:7; :: thesis: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds K . x = J * (x * (I "))
let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: K . x = J * (x * (I "))
thus K . x = L . (H . x) by FUNCT_2:15
.= J * (H . x) by A3
.= J * (x * (I ")) by A2 ; :: thesis: verum