Evaluation defines a bounded scalar-linear map into the bidual

By the operator-norm lemma, the space $X^{\ast }$ of bounded scalar-linear maps $X\to \mathbb{K}$ is itself a normed vector space. Therefore its dual $(X^{\ast }{)}^{\ast }$ is defined; this is the meaning of $X^{\ast \ast }$.

Fix $x\in X$. For $a,b\in \mathbb{K}$ and $f,g\in X^{\ast }$, evaluation gives $(af+bg)(x)=af(x)+bg(x)$, so the map $E_x:f\mapsto f(x)$ is scalar-linear. If $x\mathrm{\ne }0$, $\mathrm{\mid }f(x)\mathrm{\mid }=\mathrm{\parallel }x\mathrm{\parallel }\mathrm{\mid }f(x\mathrm{/}\mathrm{\parallel }x\mathrm{\parallel })\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }f\mathrm{\parallel }$; if $x=0$, $f(x)=0$. Thus $E_x$ is bounded and belongs to $X^{\ast \ast }$.

Define $J_X(x)=E_x$. For $x,y\in X$ and $a,b\in \mathbb{K}$, evaluating at every $f\in X^{\ast }$ gives $J_X(ax+by)(f)=f(ax+by)=a{J}_X(x)(f)+b{J}_X(y)(f)$. Equality at all arguments is equality of functions, hence $J_X$ is scalar-linear.

Taking the supremum of $\mathrm{\mid }{E}_x(f)\mathrm{\mid }\le \mathrm{\parallel }x\mathrm{\parallel }\mathrm{\parallel }f\mathrm{\parallel }$ over $\mathrm{\parallel }f\mathrm{\parallel }\le 1$ yields $\mathrm{\parallel }{J}_{X}x\mathrm{\parallel }\le \mathrm{\parallel }x\mathrm{\parallel }$. This also proves boundedness of $J_X$ with constant one. At $x=0$, $E_0$ is the zero functional and has norm zero. No step required HB or completeness.