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.||
proof
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;
hence ||.h.|| <= ||.g.|| * ||.f.|| by A8, SEQ_4:45; :: thesis: verum