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;

now :: thesis: for s being Real st s in PreNorms g holds
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;

then upper_bound (PreNorms g) <= ||.y.|| by SEQ_4:45;
then A2: ||.f.|| <= ||.y.|| by AS, Th24;
A31: ||.y.|| <= ||.f.||

proof

per cases ( ||.y.|| = 0 or ||.y.|| <> 0 ) ;

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

hence ||.y.|| <= ||.f.|| by Th27; :: thesis: verum

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;

end;

end;

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