theorem :: DUALSP04:35

for X being RealUnitarySpace
for f being linear-Functional of X
for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds
f is Lipschitzian