let X be non empty set ; :: thesis: for f being Function of X,REAL st f | X is bounded holds
( not PreNorms f is empty & PreNorms f is bounded_above )
let f be Function of X,REAL ; :: thesis: ( f | X is bounded implies ( not PreNorms f is empty & PreNorms f is bounded_above ) )
assume f | X is bounded ; :: thesis: ( not PreNorms f is empty & 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;

now

let r be real number ; :: thesis: ( r in PreNorms f implies 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

end;

hence ( not PreNorms f is empty & PreNorms f is bounded_above ) by SEQ_4:def 1; :: thesis: verum