theorem IS04A: :: LOPBAN12:15

for X, Y, Z being RealNormSpace ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . <*x,y*> = (u . x) . y ) ) ) )