let X be non empty set ; :: thesis: for Y being ComplexNormSpace

for g being Function of X, the carrier of Y holds

( g is bounded iff PreNorms g is bounded_above )

let Y be ComplexNormSpace; :: 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 )

for g being Function of X, the carrier of Y holds

( g is bounded iff PreNorms g is bounded_above )

let Y be ComplexNormSpace; :: 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 :: thesis: ( PreNorms g is bounded_above implies ex K being Real st g is bounded )

hence
( g is bounded iff PreNorms g is bounded_above )
by Th12; :: thesis: verumreconsider K = upper_bound (PreNorms g) as Real ;

assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is bounded

A2: 0 <= K

end;assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is bounded

A2: 0 <= K

proof

take K = K; :: thesis: g is bounded
consider r0 being object such that

A3: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A3;

hence 0 <= K by A1, A3, SEQ_4:def 1; :: thesis: verum

end;A3: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A3;

now :: thesis: for r being Real st r in PreNorms g holds

0 <= r

then
0 <= r0
by A3;0 <= r

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )

assume r in PreNorms g ; :: thesis: 0 <= r

then ex t being Element of X st r = ||.(g . t).|| ;

hence 0 <= r by CLVECT_1:105; :: thesis: verum

end;assume r in PreNorms g ; :: thesis: 0 <= r

then ex t being Element of X st r = ||.(g . t).|| ;

hence 0 <= r by CLVECT_1:105; :: thesis: verum

hence 0 <= K by A1, A3, SEQ_4:def 1; :: thesis: verum

now :: thesis: for t being Element of X holds ||.(g . t).|| <= K

hence
g is bounded
by A2; :: thesis: verumlet t be Element of X; :: thesis: ||.(g . t).|| <= K

||.(g . t).|| in PreNorms g ;

hence ||.(g . t).|| <= K by A1, SEQ_4:def 1; :: thesis: verum

end;||.(g . t).|| in PreNorms g ;

hence ||.(g . t).|| <= K by A1, SEQ_4:def 1; :: thesis: verum