let X be RealHilbertSpace; :: thesis:
let f be Point of (DualSp X); :: thesis:
let g be Lipschitzian linear-Functional of X; :: thesis:
assume AS: g = f ; :: thesis:
consider y being Point of X such that
A1: for x being Point of X holds g . x = x .|. y by Th89A;

now :: thesis:

let s be Real; :: thesis:
assume s in PreNorms g ; :: thesis:
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:

end;

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

proof

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

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

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

end;

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

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:

end;

end;

end;

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