theorem Th39: :: LOPBAN14:38

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