let X be non empty set ; :: thesis: for f being Function of X,COMPLEX holds
( f | X is bounded iff PreNorms f is bounded_above )
let f be Function of X,COMPLEX; :: 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 ;

A2: now

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

end;

take K = K; :: thesis: f | X is bounded
thus f | X is bounded by A2, CFUNCT_1:69; :: thesis: verum

end;

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