( 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 Lipschitzian LinearOperator of X,Z ) by LOPBAN_1:def 14, 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 9; :: thesis: verum