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 )

( 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 )

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

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

0 <= K

end;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 * ||.t.||

take K = K; :: thesis: g is Lipschitzian let t be VECTOR of X; :: thesis: |.(g . b_{1}).| <= K * ||.b_{1}.||

end;per cases
( t = 0. X or t <> 0. X )
;

end;

suppose A3:
t = 0. X
; :: thesis: |.(g . b_{1}).| <= K * ||.b_{1}.||

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 * ||.t.|| by A4, COMPLEX1:44; :: thesis: verum

end;g . t = g . (0 * (0. X)) by A3

.= 0 * (g . (0. X)) by HAHNBAN:def 3

.= 0 ;

hence |.(g . t).| <= K * ||.t.|| by A4, COMPLEX1:44; :: thesis: verum

suppose A5:
t <> 0. X
; :: thesis: |.(g . b_{1}).| <= K * ||.b_{1}.||

reconsider t1 = (||.t.|| ") * t as VECTOR of X ;

A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

A7: (|.(g . t).| / ||.t.||) * ||.t.|| = (|.(g . t).| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def 9

.= |.(g . t).| * ((||.t.|| ") * ||.t.||)

.= |.(g . t).| * 1 by A6, XCMPLX_0:def 7

.= |.(g . t).| ;

A8: |.(||.t.|| ").| = |.(1 * (||.t.|| ")).|

.= |.(1 / ||.t.||).| by XCMPLX_0:def 9

.= 1 / ||.t.|| by ABSVALUE:def 1

.= 1 * (||.t.|| ") by XCMPLX_0:def 9

.= ||.t.|| " ;

||.t1.|| = |.(||.t.|| ").| * ||.t.|| by NORMSP_1:def 1

.= 1 by A6, A8, XCMPLX_0:def 7 ;

then A9: |.(g . t1).| in { |.(g . s).| where s is VECTOR of X : ||.s.|| <= 1 } ;

|.(g . t).| / ||.t.|| = |.(g . t).| * (||.t.|| ") by XCMPLX_0:def 9

.= |.((||.t.|| ") * (g . t)).| by A8, COMPLEX1:65

.= |.(g . t1).| by HAHNBAN:def 3 ;

then |.(g . t).| / ||.t.|| <= K by A1, A9, SEQ_4:def 1;

hence |.(g . t).| <= K * ||.t.|| by A7, XREAL_1:64; :: thesis: verum

end;A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

A7: (|.(g . t).| / ||.t.||) * ||.t.|| = (|.(g . t).| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def 9

.= |.(g . t).| * ((||.t.|| ") * ||.t.||)

.= |.(g . t).| * 1 by A6, XCMPLX_0:def 7

.= |.(g . t).| ;

A8: |.(||.t.|| ").| = |.(1 * (||.t.|| ")).|

.= |.(1 / ||.t.||).| by XCMPLX_0:def 9

.= 1 / ||.t.|| by ABSVALUE:def 1

.= 1 * (||.t.|| ") by XCMPLX_0:def 9

.= ||.t.|| " ;

||.t1.|| = |.(||.t.|| ").| * ||.t.|| by NORMSP_1:def 1

.= 1 by A6, A8, XCMPLX_0:def 7 ;

then A9: |.(g . t1).| in { |.(g . s).| where s is VECTOR of X : ||.s.|| <= 1 } ;

|.(g . t).| / ||.t.|| = |.(g . t).| * (||.t.|| ") by XCMPLX_0:def 9

.= |.((||.t.|| ") * (g . t)).| by A8, COMPLEX1:65

.= |.(g . t1).| by HAHNBAN:def 3 ;

then |.(g . t).| / ||.t.|| <= K by A1, A9, SEQ_4:def 1;

hence |.(g . t).| <= K * ||.t.|| by A7, XREAL_1:64; :: thesis: verum

0 <= K

proof

hence
g is Lipschitzian
by A2; :: thesis: verum
consider r0 being object such that

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

reconsider r0 = r0 as Real by A10;

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

end;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

then
0 <= r0
by A10;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).| & ||.t.|| <= 1 ) ;

hence 0 <= r by COMPLEX1:46; :: thesis: verum

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

then ex t being VECTOR of X st

( r = |.(g . t).| & ||.t.|| <= 1 ) ;

hence 0 <= r by COMPLEX1:46; :: thesis: verum

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