theorem
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_BoundedBilinearOperators (X,Y,Z)) st
(
I is
bijective & ( 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 ) ) ) )