theorem Th7: :: LOPBAN_2:7
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h