let X, Y, Z be RealNormSpace; :: thesis: for f being bounded LinearOperator of X,Y
for g being bounded LinearOperator of Y,Z holds
( g * f is bounded LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm X,Z) . (g * f) <= ((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f) ) ) )
let f be bounded LinearOperator of X,Y; :: thesis: for g being bounded LinearOperator of Y,Z holds
( g * f is bounded LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm X,Z) . (g * f) <= ((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f) ) ) )
let g be bounded LinearOperator of Y,Z; :: thesis: ( g * f is bounded LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm X,Z) . (g * f) <= ((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f) ) ) )
reconsider ff = f as Point of (R_NormSpace_of_BoundedLinearOperators X,Y) by LOPBAN_1:def 10;
reconsider gg = g as Point of (R_NormSpace_of_BoundedLinearOperators Y,Z) by LOPBAN_1:def 10;

A1: now

let v be VECTOR of X; :: thesis: ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.||
0 <= ||.gg.|| by NORMSP_1:8;
then A2: ||.gg.|| * ||.(f . v).|| <= ||.gg.|| * (||.ff.|| * ||.v.||) by LOPBAN_1:38, XREAL_1:66;
( ||.((g * f) . v).|| = ||.(g . (f . v)).|| & ||.(g . (f . v)).|| <= ||.gg.|| * ||.(f . v).|| ) by FUNCT_2:21, LOPBAN_1:38;
hence ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.|| by A2, XXREAL_0:2; :: thesis: verum

end;

A3: ( 0 <= ||.gg.|| & 0 <= ||.ff.|| ) by NORMSP_1:8;
then reconsider gf = g * f as bounded LinearOperator of X,Z by A1, Th1, LOPBAN_1:def 9;
set K = ||.gg.|| * ||.ff.||;
A4: ( (BoundedLinearOperatorsNorm X,Y) . f = ||.ff.|| & (BoundedLinearOperatorsNorm Y,Z) . g = ||.gg.|| ) by NORMSP_1:def 1;

A5: now

let t be VECTOR of X; :: thesis: ( ||.t.|| <= 1 implies ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| )
assume ||.t.|| <= 1 ; :: thesis: ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.||
then A6: (||.gg.|| * ||.ff.||) * ||.t.|| <= (||.gg.|| * ||.ff.||) * 1 by A3, XREAL_1:66;
||.((g * f) . t).|| <= (||.gg.|| * ||.ff.||) * ||.t.|| by A1;
hence ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| by A6, XXREAL_0:2; :: thesis: verum

end;

A7: now

let r be Real; :: thesis: ( r in PreNorms gf implies r <= ||.gg.|| * ||.ff.|| )
assume r in PreNorms gf ; :: thesis: r <= ||.gg.|| * ||.ff.||
then ex t being VECTOR of X st
( r = ||.(gf . t).|| & ||.t.|| <= 1 ) ;
hence r <= ||.gg.|| * ||.ff.|| by A5; :: thesis: verum

end;

( ( for s being real number st s in PreNorms gf holds
s <= ||.gg.|| * ||.ff.|| ) implies sup (PreNorms gf) <= ||.gg.|| * ||.ff.|| ) by SEQ_4:62;
hence ( g * f is bounded LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm X,Z) . (g * f) <= ((BoundedLinearOperatorsNorm Y,Z) . g) * ((BoundedLinearOperatorsNorm X,Y) . f) ) ) ) by A1, A4, A7, LOPBAN_1:36; :: thesis: verum