theorem Th32: :: DUALSP01:26

for X being RealNormSpace
for f being Point of (DualSp X)
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||