theorem Th12: :: LOPBAN_2:12

for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a being Real holds a * (f * g) = (a * f) * g