let X, Y, Z be ComplexNormSpace; :: thesis:
let f be bounded LinearOperator of X,Y; :: thesis:
let g be bounded LinearOperator of Y,Z; :: thesis:
reconsider ff = f as Point of (C_NormSpace_of_BoundedLinearOperators X,Y) by CLOPBAN1:def 8;
reconsider gg = g as Point of (C_NormSpace_of_BoundedLinearOperators Y,Z) by CLOPBAN1:def 8;

A1: now

let v be VECTOR of X; :: thesis:
A2: ||.((g * f) . v).|| = ||.(g . (f . v)).|| by FUNCT_2:21;
A3: ||.(g . (f . v)).|| <= ||.gg.|| * ||.(f . v).|| by CLOPBAN1:36;
0 <= ||.gg.|| by CLVECT_1:106;
then ||.gg.|| * ||.(f . v).|| <= ||.gg.|| * (||.ff.|| * ||.v.||) by CLOPBAN1:36, XREAL_1:66;
hence ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.|| by A2, A3, XXREAL_0:2; :: thesis:

end;

( 0 <= ||.gg.|| & 0 <= ||.ff.|| ) by CLVECT_1:106;
then A4: 0 <= ||.gg.|| * ||.ff.|| ;
set K = ||.gg.|| * ||.ff.||;

A5: now

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

end;

reconsider gf = g * f as bounded LinearOperator of X,Z by A1, A4, Th1, CLOPBAN1:def 7;

A8: now

let r be Real; :: thesis:
assume A9: r in PreNorms gf ; :: thesis:
consider t being VECTOR of X such that
A10: ( r = ||.(gf . t).|| & ||.t.|| <= 1 ) by A9;
thus r <= ||.gg.|| * ||.ff.|| by A5, A10; :: thesis:

end;