(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
hence (modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z) by LOPBAN_1:def 9; :: thesis: verum