theorem :: NDIFF_8:10

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