let V be RealNormSpace; :: thesis: for x being Point of V
for y being Point of (DualSp V) holds |.(x .|. y).| <= ||.y.|| * ||.x.||
let x be Point of V; :: thesis: for y being Point of (DualSp V) holds |.(x .|. y).| <= ||.y.|| * ||.x.||
let y be Point of (DualSp V); :: thesis: |.(x .|. y).| <= ||.y.|| * ||.x.||
reconsider y0 = y as Lipschitzian linear-Functional of V by DUALSP01:def 10;
|.(y0 . x).| <= ||.y.|| * ||.x.|| by DUALSP01:26;
hence |.(x .|. y).| <= ||.y.|| * ||.x.|| ; :: thesis: verum