theorem
for
X,
Y,
Z being
RealNormSpace ex
I being
BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (X,Y)),
(R_NormSpace_of_BoundedLinearOperators (Y,Z)),
(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
(
I is_continuous_on the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
I . (
u,
v)
= v * u ) )