Proof of The Bolzano-Weierstrass Theorem in $\mathbb{R}^n$

Each result cited is universally quantified over the data in its own statement. No choice principle is used: the induction below proves an existential statement for each $k$, and no sequence of choices is formed.

Let $n$ and $d_{E}$ be as in the statement; $(\mathbb{R}^{n},d_{E})$ is a metric space by $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence §metric, so $d_{E}$ satisfies Metric Space §symmetric. Components are as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership.

Clause subsequence. Let $(x^{(m)})$ be a sequence in $\mathbb{R}^{n}$ whose set of terms is bounded in $(\mathbb{R}^{n},d_{E})$: there is a real $M$ with $d_{E}(u,v)\le M$ for all terms $u,v$.

Bounded coordinates. Let $k\in[n]$ and $m\in\mathbb{N}$. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations, $(x^{(m)}-x^{(1)})_{k}=x^{(m)}_{k}-x^{(1)}_{k}$, so by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §coordinate and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance,

$$|x^{(m)}_{k}-x^{(1)}_{k}|\le\lVert x^{(m)}-x^{(1)}\rVert=d_{E}(x^{(m)},x^{(1)})\le M,$$

hence $|x^{(m)}_{k}|\le M_{k}$ with $M_{k}=M+|x^{(1)}_{k}|$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value. So for every strictly increasing $\sigma:\mathbb{N}\to\mathbb{N}$ the real sequence $m\mapsto x^{(\sigma(m))}_{k}$ (a map $\mathbb{N}\to\mathbb{R}$ by Sets and Maps: Ordinary Notation §maps, its condition being predicative by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §value-substitution) is bounded, with the bound $M_{k}$.

Induction on the number of coordinates. For $k\in\mathbb{N}_{0}$ with $k\le n$ let $S(k)$ be the statement: there is a strictly increasing map $\sigma:\mathbb{N}\to\mathbb{N}$ such that for every $i\in[k]$ the real sequence $m\mapsto x^{(\sigma(m))}_{i}$ is convergent in the sense of Convergent Sequences of Real Numbers §converges. We prove $S(k)$ for every $k\le n$ by induction from $0$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction, applied to the class $\{k\in\mathbb{N}_{0}:k\le n\Rightarrow S(k)\}$; it is formed by a predicative formula with set parameters only ($n$ and the sequence $(x^{(m)})$), as $S(k)$ quantifies over sets only (maps $\mathbb{N}\to\mathbb{N}$, natural numbers and elements of $\mathbb{R}$).

$S(0)$: $[0]$ is empty by Intervals of Natural Numbers §segment, and the identity map of $\mathbb{N}$ is strictly increasing.

Let $k<n$ and assume $S(k)$, witnessed by $\sigma$. Let $c$ be the real sequence $m\mapsto x^{(\sigma(m))}_{k+1}$ (note $k+1\in[n]$ since $k<n$); it is bounded, as shown above, so by Completeness of the Real Numbers for Sequences: Monotone Convergence, the Bolzano-Weierstrass Theorem and Cauchy Sequences §bolzano-weierstrass it has a convergent subsequence, that is, there is a strictly increasing $\tau:\mathbb{N}\to\mathbb{N}$ with $c\circ\tau$ convergent. Let $\sigma'=\sigma\circ\tau$, strictly increasing by Monotone Sequences and Subsequences: Comparison of All Terms, Growth of the Indices, and Subsequences of Subsequences §composition. For $i=k+1$, the sequence $l\mapsto x^{(\sigma'(l))}_{k+1}$ is $c\circ\tau$, convergent. For $i\in[k]$, the sequence $e:m\mapsto x^{(\sigma(m))}_{i}$ converges to some real $L$ by $S(k)$; by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §real-line it converges to $L$ in $(\mathbb{R},d_{\mathbb{R}})$; its subsequence $e\circ\tau$, which is $l\mapsto x^{(\sigma'(l))}_{i}$, converges to $L$ in $(\mathbb{R},d_{\mathbb{R}})$ by the background of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §background, hence converges to $L$ by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §real-line. As $i\in[k+1]$ means $i\in[k]$ or $i=k+1$, $\sigma'$ witnesses $S(k+1)$.

Conclusion. By $S(n)$ there is a strictly increasing $\sigma:\mathbb{N}\to\mathbb{N}$ such that, for every $i\in[n]$, the real sequence $m\mapsto x^{(\sigma(m))}_{i}$ is convergent, hence convergent in $(\mathbb{R},d_{\mathbb{R}})$ by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §real-line. For $i\in[n]$ let $y_{i}=\lim_{m\to\infty}x^{(\sigma(m))}_{i}$, its limit in $(\mathbb{R},d_{\mathbb{R}})$, unique by the same background clause, to which the sequence converges by The Limit of a Convergent Sequence in a Metric Space §converges-to-limit. Let $y\in\mathbb{R}^{n}$ be the map $i\mapsto y_{i}$ on $[n]$, given by Sets and Maps: Ordinary Notation §maps and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. The subsequence $(x^{(\sigma(m))})_{m\in\mathbb{N}}$ of $(x^{(m)})$, per Subsequences §subsequence, has $k$-th coordinate sequence $m\mapsto x^{(\sigma(m))}_{k}$ converging to $y_{k}$ in $(\mathbb{R},d_{\mathbb{R}})$ for every $k\in[n]$, so it converges to $y$ in $(\mathbb{R}^{n},d_{E})$ by $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence §coordinatewise, and it is convergent.

Clause sequentially-compact. Let $K\subseteq\mathbb{R}^{n}$ be closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ and bounded in $(\mathbb{R}^{n},d_{E})$, with a real $M$ such that $d_{E}(u,v)\le M$ for all $u,v\in K$. Let $(x_{m})$ be a sequence in $\mathbb{R}^{n}$ with $x_{m}\in K$ for every $m\in\mathbb{N}$. Its set of terms is a subset of $K$, hence bounded with the same $M$ by Bounded Subset of a Metric Space §bounded. By the clause subsequence, proved above, there are a strictly increasing $\sigma:\mathbb{N}\to\mathbb{N}$ and $x\in\mathbb{R}^{n}$ such that $(x_{\sigma(k)})_{k\in\mathbb{N}}$ converges to $x$ in $(\mathbb{R}^{n},d_{E})$.

We show $x\in K$. Suppose $x\notin K$. Since $K$ is closed, $\mathbb{R}^{n}\setminus K\in\mathcal{T}_{d_{E}}$ by Closed Subset of a Topological Space §closed, so $\mathbb{R}^{n}\setminus K$ is open in $(\mathbb{R}^{n},d_{E})$ by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology. In this order: as $x\in\mathbb{R}^{n}\setminus K$, Open Subset of a Metric Space §open gives a real $r>0$ with $B_{d_{E}}(x,r)\subseteq\mathbb{R}^{n}\setminus K$; then Convergent Sequence in a Metric Space §converges with $\varepsilon=r$ gives $N\in\mathbb{N}$ with $d_{E}(x_{\sigma(k)},x)<r$ for every $k\ge N$. In particular $d_{E}(x,x_{\sigma(N)})=d_{E}(x_{\sigma(N)},x)<r$, so $x_{\sigma(N)}\in B_{d_{E}}(x,r)$ by Open Ball in a Metric Space §membership, whence $x_{\sigma(N)}\notin K$, contradicting $x_{\sigma(N)}\in K$. Hence $x\in K$, and $K$ is sequentially compact in $(\mathbb{R}^{n},d_{E})$.