let X be ComplexNormSpace; :: thesis: for f, g, h being Element of BoundedLinearOperators X,X holds f * (g * h) = (f * g) * h
let f, g, h be Element of BoundedLinearOperators X,X; :: thesis: f * (g * h) = (f * g) * h
modetrans (g * h),X,X = (modetrans g,X,X) * (modetrans h,X,X) by CLOPBAN1:def 10;
then (modetrans f,X,X) * (modetrans (g * h),X,X) = ((modetrans f,X,X) * (modetrans g,X,X)) * (modetrans h,X,X) by Th5;
hence f * (g * h) = (f * g) * h by CLOPBAN1:def 10; :: thesis: verum