let X be RealNormSpace; :: thesis: for g being linear-Functional of X holds
( g is Lipschitzian iff PreNorms g is bounded_above )

let g be linear-Functional of X; :: thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )
now :: thesis: ( PreNorms g is bounded_above implies ex K being Real st g is Lipschitzian )
reconsider K = upper_bound () as Real ;
assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is Lipschitzian
A2: now :: thesis: for t being VECTOR of X holds |.(g . t).| <= K *
let t be VECTOR of X; :: thesis: |.(g . b1).| <= K * ||.b1.||
per cases ( t = 0. X or t <> 0. X ) ;
suppose A3: t = 0. X ; :: thesis: |.(g . b1).| <= K * ||.b1.||
then A4: ||.t.|| = 0 ;
g . t = g . (0 * (0. X)) by A3
.= 0 * (g . (0. X)) by HAHNBAN:def 3
.= 0 ;
hence |.(g . t).| <= K * by ; :: thesis: verum
end;
suppose A5: t <> 0. X ; :: thesis: |.(g . b1).| <= K * ||.b1.||
reconsider t1 = () * t as VECTOR of X ;
A6: ||.t.|| <> 0 by ;
A7: (|.(g . t).| / ) * = (|.(g . t).| * ()) * by XCMPLX_0:def 9
.= |.(g . t).| * (() * )
.= |.(g . t).| * 1 by
.= |.(g . t).| ;
A8: |.().| = |.(1 * ()).|
.= |.(1 / ).| by XCMPLX_0:def 9
.= 1 / by ABSVALUE:def 1
.= 1 * () by XCMPLX_0:def 9
.= " ;
||.t1.|| = |.().| * by NORMSP_1:def 1
.= 1 by ;
then A9: |.(g . t1).| in { |.(g . s).| where s is VECTOR of X : <= 1 } ;
|.(g . t).| / = |.(g . t).| * () by XCMPLX_0:def 9
.= |.(() * (g . t)).| by
.= |.(g . t1).| by HAHNBAN:def 3 ;
then |.(g . t).| / <= K by ;
hence |.(g . t).| <= K * by ; :: thesis: verum
end;
end;
end;
take K = K; :: thesis: g is Lipschitzian
0 <= K
proof
consider r0 being object such that
A10: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A10;
now :: thesis: for r being Real st r in PreNorms g holds
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 VECTOR of X st
( r = |.(g . t).| & <= 1 ) ;
hence 0 <= r by COMPLEX1:46; :: thesis: verum
end;
then 0 <= r0 by A10;
hence 0 <= K by ; :: thesis: verum
end;
hence g is Lipschitzian by A2; :: thesis: verum
end;
hence ( g is Lipschitzian iff PreNorms g is bounded_above ) ; :: thesis: verum