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;
take K ; :: according to SEQ_4:def 1 :: thesis: for b₁ being set holds
( not b₁ in PreNorms g or b₁ <= K )

now

let r be Real; :: thesis: ( r in PreNorms g implies r <= K )
assume r in PreNorms g ; :: thesis: r <= K
then ex t being Element of X st r = ||.(g . t).|| ;
hence r <= K by A1; :: thesis: verum

end;

hence for b₁ being set holds
( not b₁ in PreNorms g or b₁ <= K ) ; :: thesis: verum

end;

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