let X, Y, Z, W be RealNormSpace; :: thesis: for f being Element of BoundedLinearOperators (Z,W)
for g being Element of BoundedLinearOperators (Y,Z)
for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h
let f be Element of BoundedLinearOperators (Z,W); :: thesis: for g being Element of BoundedLinearOperators (Y,Z)
for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h
let g be Element of BoundedLinearOperators (Y,Z); :: thesis: for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h
let h be Element of BoundedLinearOperators (X,Y); :: thesis: f * (g * h) = (f * g) * h
modetrans ((g * h),X,Z) = (modetrans (g,Y,Z)) * (modetrans (h,X,Y)) by LOPBAN_1:def 11;
then (modetrans (f,Z,W)) * (modetrans ((g * h),X,Z)) = ((modetrans (f,Z,W)) * (modetrans (g,Y,Z))) * (modetrans (h,X,Y)) by RELAT_1:36;
hence f * (g * h) = (f * g) * h by LOPBAN_1:def 11; :: thesis: verum