(modetrans g,Y,Z) * (modetrans f,X,Y) is bounded 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 10; :: thesis: verum