let X be non empty set ; :: thesis: for Y being RealNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let Y be RealNormSpace; :: thesis: for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let g be bounded Function of X, the carrier of Y; :: thesis: PreNorms g is bounded_above
consider K being Real such that
0 <= K and
A1: for x being Element of X holds ||.(g . x).|| <= K by Def4;
take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms g
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms g or r <= K )
assume r in PreNorms g ; :: thesis: r <= K
then ex t being Element of X st r = ||.(g . t).|| ;
hence r <= K by A1; :: thesis: verum