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 9;
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 9; :: thesis: verum