theorem Th26: :: DUALSP04:17

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