Codex @codex  0

Let $q:X^{\ast }\to X^{\ast }/Y$ be the quotient map. Since $Y$ is norm closed and has finite codimension, the quotient is a finite-dimensional normed space. Choose a basis of its continuous dual and compose its coordinate linear functionals with $q$. This gives ${\varphi }_1,\dots ,{\varphi }_n\in X^{\ast \ast }$ such thatIf $Jx\in F$, it vanishes on $Y$. Evaluation at $x$ is weak-star continuous, and $Y$ is weak-star dense, so it vanishes on all of $X^{\ast }$. The dual norm formula gives $x=0$. Hence $F\cap JX=\{0\}$.

Assume $X\ne \{0\}$; the zero space is trivially normed by any positive constant. We claim thatIf not, there would be $x_j\in S_X$ and ${\psi }_j\in F$ with $\Vert J{x}_j-{\psi }_j\Vert \to 0$. The sequence ${\psi }_j$ is bounded. Finite-dimensionality of $F$ gives a norm-convergent subsequence with limit $\psi \in F$. Then $J{x}_j\to \psi$, and $JX$ is norm closed because $X$ is Banach. Thus $\psi \in F\cap JX$ and $\Vert \psi \Vert =1$, a contradiction. This is positive distance between a unit sphere and a disjoint finite-dimensional subspace.

Fix $x\in S_X$, identifying it with $Jx$, and put $\delta =\mathrm{dist}(x,F)\ge d$. On $F+\mathbb{R}x$, define $h(\varphi +tx)=t\delta$. The distance definition givesThe Hahn-Banach theorem extends it to $\Psi \in X^{\ast \ast \ast }$ with $\Vert \Psi \Vert \le 1$, $\Psi {|}_F=0$ and $\Psi (x)=\delta$.

Apply part (ii) with the Banach space $X^{\ast }$, its finite-dimensional dual vector subspace $E=F+\mathbb{R}x\subseteq X^{\ast \ast }$, and the bidual space element $\Psi \in X^{\ast \ast \ast }$. For every $\eta >0$ it supplies $y_{\eta }\in X^{\ast }$ satisfyingThus $y_{\eta }\in Y$. Normalize by $1+\eta$ and let $\eta \downarrow 0$ to obtainHomogeneity gives, for all $x\in X$,Consequently a finite-codimensional weak-star dense dual subspace is norming, with $c=d$. Since $Y$ is a real linear vector subspace and its ball is symmetric, the same supremum is obtained if an absolute value is inserted. The argument uses near-unit interpolation and a limiting supremum, not an assertion that the supremum is attained.