let X be RealUnitarySpace; :: thesis: for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above
let g be Lipschitzian linear-Functional of X; :: thesis: PreNorms g is bounded_above
consider K being Real such that
A1: ( 0 < K & ( for x being VECTOR of X holds |.(g . x).| <= K * ||.x.|| ) ) by BHSP_6:def 4;
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 consider t being VECTOR of X such that
A3: ( r = |.(g . t).| & ||.t.|| <= 1 ) ;
A5: |.(g . t).| <= K * ||.t.|| by A1;
K * ||.t.|| <= K * 1 by A1, A3, XREAL_1:64;
hence r <= K by A3, A5, XXREAL_0:2; :: thesis: verum