let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for g being bounded Function of X,the carrier of Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )
let Y be ComplexNormSpace; :: thesis: for g being bounded Function of X,the carrier of Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )
let g be bounded Function of X,the carrier of Y; :: thesis: ( not PreNorms g is empty & PreNorms g is bounded_above )
PreNorms g is bounded_above

proof

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

A2: now

let r be Real; :: thesis: ( r in PreNorms g implies r <= K )
assume A3: r in PreNorms g ; :: thesis: r <= K
consider t being Element of X such that
A4: r = ||.(g . t).|| by A3;
thus r <= K by A1, A4; :: 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 A2; :: thesis: verum

end;

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