theorem Th38:
for
E,
F,
G being
RealNormSpace ex
B being
Lipschitzian BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (E,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (E,G)) st
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (E,F)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) holds
B . (
u,
v)
= v * u