( R_NormSpace_of_BoundedLinearOperators X,Z = NORMSTR(# (BoundedLinearOperators X,Z),(Zero_ (BoundedLinearOperators X,Z),(R_VectorSpace_of_LinearOperators X,Z)),(Add_ (BoundedLinearOperators X,Z),(R_VectorSpace_of_LinearOperators X,Z)),(Mult_ (BoundedLinearOperators X,Z),(R_VectorSpace_of_LinearOperators X,Z)),(BoundedLinearOperatorsNorm X,Z) #) & (modetrans g,Y,Z) * (modetrans f,X,Y) is bounded LinearOperator of X,Z ) by LOPBAN_1:def 15, LOPBAN_2:2;
hence (modetrans g,Y,Z) * (modetrans f,X,Y) is Point of (R_NormSpace_of_BoundedLinearOperators X,Z) by LOPBAN_1:def 10; :: thesis: verum