theorem :: LOPBAN13:27

for X, Y, Z being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u