theorem :: LOPBAN12:10

for X, Y, Z being RealLinearSpace ex I being LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & ( for u being Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
for x being Point of X
for y being Point of Y holds (I . u) . <*x,y*> = (u . x) . y ) )