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

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

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

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

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

let g be Lipschitzian linear-Functional of X; :: thesis: ( g = f implies ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| ) )

assume AS: g = f ; :: thesis: ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

consider y being Point of X such that

A1: for x being Point of X holds g . x = x .|. y by Th89A;

then A2: ||.f.|| <= ||.y.|| by AS, Th24;

A31: ||.y.|| <= ||.f.||

thus ( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| ) by A1, A2, XXREAL_0:1, A31; :: thesis: verum

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

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

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

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

let g be Lipschitzian linear-Functional of X; :: thesis: ( g = f implies ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| ) )

assume AS: g = f ; :: thesis: ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

consider y being Point of X such that

A1: for x being Point of X holds g . x = x .|. y by Th89A;

now :: thesis: for s being Real st s in PreNorms g holds

s <= ||.y.||

then
upper_bound (PreNorms g) <= ||.y.||
by SEQ_4:45;s <= ||.y.||

let s be Real; :: thesis: ( s in PreNorms g implies s <= ||.y.|| )

assume s in PreNorms g ; :: thesis: s <= ||.y.||

then consider t being VECTOR of X such that

B1: ( s = |.(g . t).| & ||.t.|| <= 1 ) ;

B3: |.(t .|. y).| <= ||.t.|| * ||.y.|| by BHSP_1:29;

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

then ||.t.|| * ||.y.|| <= 1 * ||.y.|| by B1, XREAL_1:64;

then |.(t .|. y).| <= ||.y.|| by B3, XXREAL_0:2;

hence s <= ||.y.|| by B1, A1; :: thesis: verum

end;assume s in PreNorms g ; :: thesis: s <= ||.y.||

then consider t being VECTOR of X such that

B1: ( s = |.(g . t).| & ||.t.|| <= 1 ) ;

B3: |.(t .|. y).| <= ||.t.|| * ||.y.|| by BHSP_1:29;

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

then ||.t.|| * ||.y.|| <= 1 * ||.y.|| by B1, XREAL_1:64;

then |.(t .|. y).| <= ||.y.|| by B3, XXREAL_0:2;

hence s <= ||.y.|| by B1, A1; :: thesis: verum

then A2: ||.f.|| <= ||.y.|| by AS, Th24;

A31: ||.y.|| <= ||.f.||

proof
end;

take
y
; :: thesis: ( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )per cases
( ||.y.|| = 0 or ||.y.|| <> 0 )
;

end;

suppose AS2:
||.y.|| <> 0
; :: thesis: ||.y.|| <= ||.f.||

B1:
0 <= y .|. y
by BHSP_1:def 2;

B2: g . y = y .|. y by A1

.= ||.y.|| ^2 by B1, SQUARE_1:def 2

.= ||.y.|| * ||.y.|| by SQUARE_1:def 1 ;

B3: g . y <= |.(g . y).| by ABSVALUE:4;

|.(g . y).| <= ||.f.|| * ||.y.|| by AS, Th26;

then B4: ||.y.|| * ||.y.|| <= ||.f.|| * ||.y.|| by B2, B3, XXREAL_0:2;

B51: 0 <= ||.y.|| by BHSP_1:28;

( (||.y.|| * ||.y.||) / ||.y.|| = ||.y.|| & (||.f.|| * ||.y.||) / ||.y.|| = ||.f.|| ) by AS2, XCMPLX_1:89;

hence ||.y.|| <= ||.f.|| by B51, B4, XREAL_1:72; :: thesis: verum

end;B2: g . y = y .|. y by A1

.= ||.y.|| ^2 by B1, SQUARE_1:def 2

.= ||.y.|| * ||.y.|| by SQUARE_1:def 1 ;

B3: g . y <= |.(g . y).| by ABSVALUE:4;

|.(g . y).| <= ||.f.|| * ||.y.|| by AS, Th26;

then B4: ||.y.|| * ||.y.|| <= ||.f.|| * ||.y.|| by B2, B3, XXREAL_0:2;

B51: 0 <= ||.y.|| by BHSP_1:28;

( (||.y.|| * ||.y.||) / ||.y.|| = ||.y.|| & (||.f.|| * ||.y.||) / ||.y.|| = ||.f.|| ) by AS2, XCMPLX_1:89;

hence ||.y.|| <= ||.f.|| by B51, B4, XREAL_1:72; :: thesis: verum

thus ( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| ) by A1, A2, XXREAL_0:1, A31; :: thesis: verum