theorem :: NDIFF_8:4

for X, Y, Z, W being RealNormSpace
for f being Lipschitzian LinearOperator of Z,W
for g being Lipschitzian LinearOperator of Y,Z
for h being Lipschitzian LinearOperator of X,Y holds f * (g * h) = (f * g) * h by RELAT_1:36;