The Dual of a Real Normed Space is a Real Banach Space, and the Dual Norm is the Least Bound

In the setting of The Real Numbers: Standing Notation and Background, let $E$ with norm $\lVert\cdot\rVert$ be a real normed space, let $E^{*}$ be its dual space with the operations fixed there, and let $\lVert\ell\rVert_{E^{*}}$ be the dual norm of $\ell\in E^{*}$. Bounds are those of The Dual Space of a Real Normed Space and the Dual Norm §functional.

1. (Vector space)¶ $E^{*}$ with these operations is a real vector space. Its zero vector is the zero functional $v\mapsto0$, and the additive inverse of $\ell$ is $(-1)\ell$.

2. (Least bound)¶ For every $\ell\in E^{*}$ the dual norm $\lVert\ell\rVert_{E^{*}}$ is a nonnegative bound for $\ell$, that is, $|\ell(v)|\le\lVert\ell\rVert_{E^{*}}\lVert v\rVert$ for every $v\in E$, and $\lVert\ell\rVert_{E^{*}}\le C$ for every nonnegative bound $C$ for $\ell$.

3. (Normed space)¶ The map $\ell\mapsto\lVert\ell\rVert_{E^{*}}$ is a norm on the vector space of claim 1, so that $E^{*}$ with the dual norm is a real normed space.

4. (Completeness)¶ $E^{*}$ with the dual norm is a real Banach space.

5. (Weak-star limits)¶ A sequence in $E^{*}$ converges weak-star to at most one element of $E^{*}$, and a sequence in $E^{*}$ that converges to $\ell$ in the normed space of claim 3 converges weak-star to $\ell$.