let X, Y, Z, W be RealNormSpace; :: thesis: 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)); :: thesis: 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)); :: thesis: 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)); :: thesis: 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 ;
:: thesis: verum