let X be non empty set ; :: thesis: for Y being RealNormSpace
for g being Function of X,the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let Y be RealNormSpace; :: thesis: for g being Function of X,the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let g be Function of X,the carrier of Y; :: thesis: ( g is bounded iff PreNorms g is bounded_above )

now

assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is bounded
reconsider K = upper_bound (PreNorms g) as Real ;
A2: 0 <= K

proof

A3: now

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )
assume A4: r in PreNorms g ; :: thesis: 0 <= r
consider t being Element of X such that
A5: r = ||.(g . t).|| by A4;
thus 0 <= r by A5, NORMSP_1:8; :: thesis: verum

end;

consider r0 being set such that
A6: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A6;
0 <= r0 by A3, A6;
hence 0 <= K by A1, A6, SEQ_4:def 4; :: thesis: verum

end;

A7: now

let t be Element of X; :: thesis: ||.(g . t).|| <= K
||.(g . t).|| in PreNorms g ;
hence ||.(g . t).|| <= K by A1, SEQ_4:def 4; :: thesis: verum

end;

take K = K; :: thesis: g is bounded
thus g is bounded by A2, A7, Def4; :: thesis: verum

end;

hence ( g is bounded iff PreNorms g is bounded_above ) by Th13; :: thesis: verum