theorem LOPBAN1623: :: LOPBAN13:26

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) & (- w) * u = - (w * u) )