theorem LOPBAN1624: :: LOPBAN13:28

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))
for r being Real holds
( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )