Concatenation Identifies a Product of Euclidean Spaces with a Euclidean Space

Let $m,n\in\mathbb{N}$ be natural numbers and let $\mathbb{R}$ be the ordered field of real numbers. For $p\in\mathbb{N}$ regard Euclidean space $\mathbb{R}^p$ as a real vector space by Euclidean Space $\mathbb{R}^n$ is a Real Vector Space, with the sum $z+z'$, the scalar multiple $\lambda z$, and the difference $z-z'$ and dot product $z\cdot z'$; write $\lVert\,\cdot\,\rVert$ for the Euclidean norm, $\lVert z\rVert^2$ for $\lVert z\rVert\cdot\lVert z\rVert$, and $d_E$ for the Euclidean distance, a metric by Euclidean Distance is a Metric on $\mathbb{R}^n$. Let $[p]$ be the initial segment determined by $p$. Equip $\mathbb{R}^m\times\mathbb{R}^n$ with the product metric $d_{\times}$ obtained from the Euclidean distances on the two factors, a metric by claim 1 of The Product Metric is a Metric.

Every $k\in[m+n]$ satisfies exactly one of $k\in[m]$ and $k=m+j$ for a unique $j\in[n]$: this is claim 7 of Properties of the Order on the Natural Numbers together with trichotomy, claim 3 there, and, for $j\in[n]$, claims 5 and 4 of Arithmetic of Addition on the Natural Numbers. Accordingly, define the concatenation map

by letting $\iota(\xi,\eta)$, for $\xi=(\xi_1,\dots,\xi_m)$ and $\eta=(\eta_1,\dots,\eta_n)$, be the point $w\in\mathbb{R}^{m+n}$ with

Then the following hold.

1. (Bijection) $\iota$ is a bijection, with inverse the map sending $w\in\mathbb{R}^{m+n}$ to the pair whose first entry has $k$th coordinate $w_k$ for $k\in[m]$ and whose second entry has $j$th coordinate $w_{m+j}$ for $j\in[n]$.

2. (Linearity) For all $\xi,\xi'\in\mathbb{R}^m$, $\eta,\eta'\in\mathbb{R}^n$ and $\lambda\in\mathbb{R}$,

3. (Dot products and norms) For all $\xi,\xi'\in\mathbb{R}^m$ and $\eta,\eta'\in\mathbb{R}^n$,

4. (Metrics) For all $z=(\xi,\eta)$ and $z'=(\xi',\eta')$ in $\mathbb{R}^m\times\mathbb{R}^n$,

and