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 number such that
A1: for x being set st x in X /\ (dom f) holds
abs (f . x) <= K by RFUNCT_1:90;
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 ext-real number ; :: 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 = abs (f . t) ;
hence r <= K by A1, A2; :: thesis: verum