theorem :: LOPBAN12:16

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