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