A finite-dimensional normed subspace is closed

If $n=0$, then $W=\{0\}$ by [L2]. Every $x\in V\setminus \{0\}$ has the open ball of radius $\mathrm{\parallel }x\mathrm{\parallel }\mathrm{/}2$ disjoint from $W$, so its complement is open and $W$ is closed. It remains to treat $n>0$.

For $n>0$, in the real case put $m=n$ and $e_j=b_j$. In the complex case put $m=2n$, $e_{2j}=b_j$, and $e_{2j+1}=i{b}_j$, and use real scalars. Splitting complex coefficients proves real spanning; grouping a real relation into a complex relation among the $b_j$ proves independence. Thus $(e_j{)}_{j<m}$ is a supplied ordered real basis of $W$, and its norm is still the restricted ambient norm. By [L1], $W$ is complete for this metric.

Define maps $E_j:\mathbb{N}\to {\mathbb{Q}}^j$ for $j\le m$ as follows: $E_0(s)$ is the empty tuple, and $E_{j+1}(p(s,t))=(E_j(s),q(t))\mathrm{.}$ The unique inverse pair of each natural makes this a total definition. Finite recursion, or [L5] on states consisting of a stage and such a map, produces the maps uniformly; after stage $m$ keep the state fixed. By induction each $E_j$ is surjective: given a tuple of length $j+1$, its initial tuple has a preimage $s$ under $E_j$, its final coordinate has a preimage $t$ under $q$, and $p(s,t)$ maps to the entire tuple. This uses two witnesses for one tuple, not a family of selected enumerations. Define $d(s)={\sum }_{j<m}(E_m(s){)}_j{e}_j\mathrm{.}$ Its image is exactly the rational span of this finite basis.

This image is dense in $W$. For $w={\sum }_{j<m}{a}_j{e}_j$ and $\epsilon >0$, let $t_j$ be the least index satisfying $\mathrm{\mid }{a}_j-q(t_j)\mathrm{\mid }<\delta ,\delta =\frac{\epsilon }{2m(1+{\sum }_{j<m}\mathrm{\parallel }{e}_j\mathrm{\parallel })}>0.$ Existence follows from rational density and [L5] gives the least index. Surjectivity of $E_m$ gives a value of $d$ equal to $v={\sum }_{j<m}q(t_j)e_j$, and $\mathrm{\parallel }w-v\mathrm{\parallel }\le \delta {\sum }_{j<m}\mathrm{\parallel }{e}_j\mathrm{\parallel }<\epsilon \mathrm{.}$ Hence every ball in $W$ meets $d[\mathbb{N}]$.

Let $x$ be an ambient adherent point of $W$, meaning every ball about $x$ meets $W$. For each $k\in \mathbb{N}$, first such adherence and then step 3.1 give a point $w\in W$ within $1\mathrm{/}(2(k+1))$ of $x$ and a value $d(s)$ within $1\mathrm{/}(2(k+1))$ of $w$. Thus the set $A_k=\{s\in \mathbb{N}:\mathrm{\parallel }x-d(s)\mathrm{\parallel }<1\mathrm{/}(k+1)\}$ is nonempty. Set $s_k=\min A_k$ and $u_k=d(s_k)$. This defines the sequence outright by a unique-index rule. By [L6] the error tends to zero, so $u_k\to x$ in $V$, and $\mathrm{\parallel }{u}_k-u_l\mathrm{\parallel }\le \mathrm{\parallel }{u}_k-x\mathrm{\parallel }+\mathrm{\parallel }x-u_l\mathrm{\parallel }$ makes it Cauchy in the restricted metric of $W$.

Completeness from step 1.2 supplies $y\in W$ with $u_k\to y$ in the restricted norm. Since the norm agrees with the ambient one, $\mathrm{\parallel }x-y\mathrm{\parallel }\le \mathrm{\parallel }x-u_k\mathrm{\parallel }+\mathrm{\parallel }{u}_k-y\mathrm{\parallel }⟶0,$ so $x=y\in W$. Every ambient adherent point therefore belongs to $W$. A point outside $W$ consequently has a ball disjoint from $W$, making the complement open and $W$ closed. Together with step 1.1 this proves all cases, without manufacturing a sequence in an arbitrary subset or using countable choice.