let X be RealHilbertSpace; :: thesis: for f being Point of ()
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 ) & = )

let f be Point of (); :: 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 ) & = )

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 ) & = ) )

assume AS: g = f ; :: thesis: ex y being Point of X st
( ( for x being Point of X holds g . x = x .|. 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 <=
let s be Real; :: thesis: ( s in PreNorms g implies s <= )
assume s in PreNorms g ; :: thesis: s <=
then consider t being VECTOR of X such that
B1: ( s = |.(g . t).| & <= 1 ) ;
B3: |.(t .|. y).| <= * by BHSP_1:29;
0 <= by BHSP_1:28;
then ||.t.|| * <= 1 * by ;
then |.(t .|. y).| <= by ;
hence s <= by B1, A1; :: thesis: verum
end;
then upper_bound () <= by SEQ_4:45;
then A2: ||.f.|| <= by ;
A31: ||.y.|| <=
proof
per cases = 0 or <> 0 ) ;
suppose AS2: ||.y.|| <> 0 ; :: thesis:
B1: 0 <= y .|. y by BHSP_1:def 2;
B2: g . y = y .|. y by A1
.= ^2 by
.= * by SQUARE_1:def 1 ;
B3: g . y <= |.(g . y).| by ABSVALUE:4;
|.(g . y).| <= * by ;
then B4: ||.y.|| * <= * by ;
B51: 0 <= by BHSP_1:28;
( (||.y.|| * ) / = & () / = ) by ;
hence ||.y.|| <= by ; :: thesis: verum
end;
end;
end;
take y ; :: thesis: ( ( for x being Point of X holds g . x = x .|. y ) & = )
thus ( ( for x being Point of X holds g . x = x .|. y ) & = ) by ; :: thesis: verum