let E, F, G be RealNormSpace; :: thesis: for f being Point of
for g being Point of ex h being Point of st
( h = g * f & <= * )

let f be Point of ; :: thesis: for g being Point of ex h being Point of st
( h = g * f & <= * )

let g be Point of ; :: thesis: ex h being Point of st
( 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 by LOPBAN_1:def 9;
take h ; :: thesis: ( h = g * f & <= * )
thus h = g * f ; :: thesis:
A8: = 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 <= *
proof
let t be Real; :: thesis: ( t in PreNorms Lh implies t <= * )
assume t in PreNorms Lh ; :: thesis:
then consider w being Point of E such that
A9: ( t = ||.(Lh . w).|| & <= 1 ) ;
A10: ||.(Lh . w).|| = ||.(Lg . (Lf . w)).|| by FUNCT_2:15;
A11: ||.(Lf . w).|| <= * by LOPBAN_1:32;
||.f.|| * <= * 1 by ;
then A12: ||.(Lf . w).|| <= by ;
A13: ||.(Lg . (Lf . w)).|| <= * ||.(Lf . w).|| by LOPBAN_1:32;
||.g.|| * ||.(Lf . w).|| <= * by ;
hence t <= * by ; :: thesis: verum
end;
hence ||.h.|| <= * by ; :: thesis: verum