theorem
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_BilinearOperators (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 ) )