A1: 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) #) by LOPBAN_1:def 15;
(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 Point of (R_NormSpace_of_BoundedLinearOperators X,Z) by A1, LOPBAN_1:def 10; :: thesis: verum