let X be RealUnitarySpace; :: thesis: for f being Point of (DualSp X)

for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let f be Point of (DualSp X); :: thesis: for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let g be Lipschitzian linear-Functional of X; :: thesis: ( g = f implies for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.|| )

assume A1: g = f ; :: thesis: for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let t be VECTOR of X; :: thesis: |.(g . t).| <= ||.f.|| * ||.t.||

for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let f be Point of (DualSp X); :: thesis: for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let g be Lipschitzian linear-Functional of X; :: thesis: ( g = f implies for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.|| )

assume A1: g = f ; :: thesis: for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

let t be VECTOR of X; :: thesis: |.(g . t).| <= ||.f.|| * ||.t.||

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

end;

suppose A3:
t = 0. X
; :: thesis: |.(g . t).| <= ||.f.|| * ||.t.||

then A4:
||.t.|| = 0
by BHSP_1:26;

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

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

.= 0 ;

hence |.(g . t).| <= ||.f.|| * ||.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).| <= ||.f.|| * ||.t.|| by A4, COMPLEX1:44; :: thesis: verum

suppose A5:
t <> 0. X
; :: thesis: |.(g . t).| <= ||.f.|| * ||.t.||

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

A6: ||.t.|| <> 0 by A5, BHSP_1:26;

then B61: 0 < ||.t.|| by BHSP_1:28;

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

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

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

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

.= ||.t.|| " ;

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

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

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

||.t1.|| = |.(||.t.|| ").| * ||.t.|| by BHSP_1:27

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

then |.(g . t).| / ||.t.|| in { |.(g . s).| where s is VECTOR of X : ||.s.|| <= 1 } by A8;

then |.(g . t).| / ||.t.|| <= upper_bound (PreNorms g) by SEQ_4:def 1;

then A9: |.(g . t).| / ||.t.|| <= ||.f.|| by A1, Th24;

A10: (|.(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).| ;

0 <= ||.t.|| by BHSP_1:28;

hence |.(g . t).| <= ||.f.|| * ||.t.|| by A9, A10, XREAL_1:64; :: thesis: verum

end;A6: ||.t.|| <> 0 by A5, BHSP_1:26;

then B61: 0 < ||.t.|| by BHSP_1:28;

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

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

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

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

.= ||.t.|| " ;

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

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

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

||.t1.|| = |.(||.t.|| ").| * ||.t.|| by BHSP_1:27

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

then |.(g . t).| / ||.t.|| in { |.(g . s).| where s is VECTOR of X : ||.s.|| <= 1 } by A8;

then |.(g . t).| / ||.t.|| <= upper_bound (PreNorms g) by SEQ_4:def 1;

then A9: |.(g . t).| / ||.t.|| <= ||.f.|| by A1, Th24;

A10: (|.(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).| ;

0 <= ||.t.|| by BHSP_1:28;

hence |.(g . t).| <= ||.f.|| * ||.t.|| by A9, A10, XREAL_1:64; :: thesis: verum