let X, Y, Z, W be 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
let f be 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
let g be 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
let h be Point of (R_NormSpace_of_BoundedLinearOperators (Z,W)); h * (g * f) = (h * g) * f
A2:
h * g is Lipschitzian LinearOperator of Y,W
by LOPBAN_2:2;
g * f is Lipschitzian LinearOperator of X,Z
by LOPBAN_2:2;
hence h * (g * f) =
(modetrans (h,Z,W)) * ((modetrans (g,Y,Z)) * (modetrans (f,X,Y)))
by LOPBAN_1:29
.=
((modetrans (h,Z,W)) * (modetrans (g,Y,Z))) * (modetrans (f,X,Y))
by RELAT_1:36
.=
(h * g) * f
by A2, LOPBAN_1:29
;
verum