let X, Y, Z be RealNormSpace; :: thesis: for f being Lipschitzian LinearOperator of X,Y
for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian 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 Lipschitzian LinearOperator of X,Y; :: thesis: for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian 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 Lipschitzian LinearOperator of Y,Z; :: thesis: ( g * f is Lipschitzian 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 9;
reconsider gg = g as Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;

A1: now :: thesis: for v being VECTOR of X holds ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.||

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

end;

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

A4: now :: thesis: for t being VECTOR of X st ||.t.|| <= 1 holds
||.((g * f) . t).|| <= ||.gg.|| * ||.ff.||

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 A5: (||.gg.|| * ||.ff.||) * ||.t.|| <= (||.gg.|| * ||.ff.||) * 1 by A3, XREAL_1:64;
||.((g * f) . t).|| <= (||.gg.|| * ||.ff.||) * ||.t.|| by A1;
hence ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| by A5, XXREAL_0:2; :: thesis: verum

end;

A6: now :: thesis: for r being Real st r in PreNorms gf holds
r <= ||.gg.|| * ||.ff.||

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 A4; :: thesis: verum

end;

( ( for s being Real st s in PreNorms gf holds
s <= ||.gg.|| * ||.ff.|| ) implies upper_bound (PreNorms gf) <= ||.gg.|| * ||.ff.|| ) by SEQ_4:45;
hence ( g * f is Lipschitzian 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, A6, LOPBAN_1:30; :: thesis: verum