theorem LM100: :: LOPBAN13:19

for X, Y, Z being RealNormSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )