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

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 :: thesis: for t being Element of X st t in X /\ (dom f) holds
|.(f /. t).| <= K

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 Th10; :: thesis: verum