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 )

( 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 )

hence
( f | X is bounded iff PreNorms f is bounded_above )
by Th10; :: thesis: verumassume A1:
PreNorms f is bounded_above
; :: thesis: ex K being Real st f | X is bounded

reconsider K = upper_bound (PreNorms f) as Real ;

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

end;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

take K = K; :: thesis: f | X is bounded |.(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;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

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