theorem Th9: :: CLOPBAN2:9

for X being ComplexNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)