let X be RealNormSpace; :: 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 LOPBAN_1:def 12;
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 LOPBAN_1:def 12; :: thesis: verum