theorem :: DUALSP04:41

for X being RealHilbertSpace
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.|| )