let X, Y be ComplexNormSpace; :: thesis: for g being bounded LinearOperator of X,Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )
let g be bounded LinearOperator of X,Y; :: thesis: ( not PreNorms g is empty & PreNorms g is bounded_above )
PreNorms g is bounded_above

proof

consider K being Real such that
A1: 0 <= K and
A2: for x being VECTOR of X holds ||.(g . x).|| <= K * ||.x.|| by Def7;

A3: now

let r be Real; :: thesis: ( r in PreNorms g implies r <= K )
assume A4: r in PreNorms g ; :: thesis: r <= K
consider t being VECTOR of X such that
A5: ( r = ||.(g . t).|| & ||.t.|| <= 1 ) by A4;
A6: ||.(g . t).|| <= K * ||.t.|| by A2;
K * ||.t.|| <= K * 1 by A1, A5, XREAL_1:66;
hence r <= K by A5, A6, XXREAL_0:2; :: thesis: verum

end;

take K ; :: according to SEQ_4:def 1 :: thesis: for b₁ being set holds
( not b₁ in PreNorms g or b₁ <= K )
thus for b₁ being set holds
( not b₁ in PreNorms g or b₁ <= K ) by A3; :: thesis: verum

end;

hence ( not PreNorms g is empty & PreNorms g is bounded_above ) ; :: thesis: verum