theorem Th89A: :: DUALSP04:39

for X being RealHilbertSpace
for f being linear-Functional of X st f is Lipschitzian holds
ex y being Point of X st
for x being Point of X holds f . x = x .|. y