let E, F, G be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))

for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

let f be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

let g be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

reconsider Lf = f as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;

reconsider Lg = g as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;

set Lh = Lg * Lf;

reconsider Lh = Lg * Lf as Lipschitzian LinearOperator of E,G by LOPBAN_2:2;

reconsider h = Lh as Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;

take h ; :: thesis: ( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

thus h = g * f ; :: thesis: ||.h.|| <= ||.g.|| * ||.f.||

A8: ||.h.|| = upper_bound (PreNorms (modetrans (h,E,G))) by LOPBAN_1:def 13

.= upper_bound (PreNorms Lh) by LOPBAN_1:29 ;

for t being Real st t in PreNorms Lh holds

t <= ||.g.|| * ||.f.||

for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

let f be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

let g be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st

( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

reconsider Lf = f as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;

reconsider Lg = g as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;

set Lh = Lg * Lf;

reconsider Lh = Lg * Lf as Lipschitzian LinearOperator of E,G by LOPBAN_2:2;

reconsider h = Lh as Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;

take h ; :: thesis: ( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

thus h = g * f ; :: thesis: ||.h.|| <= ||.g.|| * ||.f.||

A8: ||.h.|| = upper_bound (PreNorms (modetrans (h,E,G))) by LOPBAN_1:def 13

.= upper_bound (PreNorms Lh) by LOPBAN_1:29 ;

for t being Real st t in PreNorms Lh holds

t <= ||.g.|| * ||.f.||

proof

hence
||.h.|| <= ||.g.|| * ||.f.||
by A8, SEQ_4:45; :: thesis: verum
let t be Real; :: thesis: ( t in PreNorms Lh implies t <= ||.g.|| * ||.f.|| )

assume t in PreNorms Lh ; :: thesis: t <= ||.g.|| * ||.f.||

then consider w being Point of E such that

A9: ( t = ||.(Lh . w).|| & ||.w.|| <= 1 ) ;

A10: ||.(Lh . w).|| = ||.(Lg . (Lf . w)).|| by FUNCT_2:15;

A11: ||.(Lf . w).|| <= ||.f.|| * ||.w.|| by LOPBAN_1:32;

||.f.|| * ||.w.|| <= ||.f.|| * 1 by A9, XREAL_1:64;

then A12: ||.(Lf . w).|| <= ||.f.|| by A11, XXREAL_0:2;

A13: ||.(Lg . (Lf . w)).|| <= ||.g.|| * ||.(Lf . w).|| by LOPBAN_1:32;

||.g.|| * ||.(Lf . w).|| <= ||.g.|| * ||.f.|| by A12, XREAL_1:64;

hence t <= ||.g.|| * ||.f.|| by A9, A10, A13, XXREAL_0:2; :: thesis: verum

end;assume t in PreNorms Lh ; :: thesis: t <= ||.g.|| * ||.f.||

then consider w being Point of E such that

A9: ( t = ||.(Lh . w).|| & ||.w.|| <= 1 ) ;

A10: ||.(Lh . w).|| = ||.(Lg . (Lf . w)).|| by FUNCT_2:15;

A11: ||.(Lf . w).|| <= ||.f.|| * ||.w.|| by LOPBAN_1:32;

||.f.|| * ||.w.|| <= ||.f.|| * 1 by A9, XREAL_1:64;

then A12: ||.(Lf . w).|| <= ||.f.|| by A11, XXREAL_0:2;

A13: ||.(Lg . (Lf . w)).|| <= ||.g.|| * ||.(Lf . w).|| by LOPBAN_1:32;

||.g.|| * ||.(Lf . w).|| <= ||.g.|| * ||.f.|| by A12, XREAL_1:64;

hence t <= ||.g.|| * ||.f.|| by A9, A10, A13, XXREAL_0:2; :: thesis: verum