let X be non empty set ; :: thesis: for f being Function of X,REAL holds
( f | X is bounded iff PreNorms f is bounded_above )
let f be Function of X,REAL ; :: thesis: ( f | X is bounded iff PreNorms f is bounded_above )

now

assume A1: PreNorms f is bounded_above ; :: thesis: ex K being Real st f | X is bounded
reconsider K = upper_bound (PreNorms f) as Real ;

A7: now

let t be set ; :: thesis: ( t in X /\ (dom f) implies abs (f . t) <= K )
assume t in X /\ (dom f) ; :: thesis: abs (f . t) <= K
then abs (f . t) in PreNorms f ;
hence abs (f . t) <= K by A1, SEQ_4:def 4; :: thesis: verum

end;

take K = K; :: thesis: f | X is bounded
thus f | X is bounded by A7, RFUNCT_1:90; :: thesis: verum

end;

hence ( f | X is bounded iff PreNorms f is bounded_above ) by ThB13; :: thesis: verum