let X be non empty set ; :: thesis: for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above
let f be Function of X,REAL; :: thesis: ( f | X is bounded implies PreNorms f is bounded_above )
assume f | X is bounded ; :: thesis: PreNorms f is bounded_above
then consider K being Real such that
A1: for x being object st x in X /\ (dom f) holds
|.(f . x).| <= K by RFUNCT_1:73;
A2: X /\ (dom f) = X /\ X by FUNCT_2:def 1;
take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms f
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms f or r <= K )
assume r in PreNorms f ; :: thesis: r <= K
then ex t being Element of X st r = |.(f . t).| ;
hence r <= K by A1, A2; :: thesis: verum