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 :: thesis: ( PreNorms f is bounded_above implies ex K being Real st f | X is bounded )

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

now :: thesis: for t being object st t in X /\ (dom f) holds
|.(f . t).| <= K

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

end;

hence f | X is bounded by RFUNCT_1:73; :: thesis: verum

end;

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