theorem RELAT136: :: LOPBAN13:10

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