let X be ComplexNormSpace; 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); 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; verum