theorem Th36: :: LOPBAN14:35

for X, Z being RealNormSpace
for Y being RealNormSpace-Sequence ex I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for y being Point of (product Y)
for x being Point of X holds (I . u) . (y ^ <*x*>) = (u . x) . y ) ) ) )