for X being ComplexNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)