theorem LPB2Th9: :: NDIFF_8:9

for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)