The Euclidean Distance on $\mathbb{R}^n$

In the setting of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces, let $n\in\mathbb{N}$, with the difference of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv) and the Euclidean norm $\lVert\cdot\rVert$ on $\mathbb{R}^{n}$. The map below exists and is unique by The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps (iv).

(i) The Euclidean distance on $\mathbb{R}^{n}$ is the map $d_{E}:\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ with

$$d_{E}(x,y)=\lVert x-y\rVert\qquad\text{for all }x,y\in\mathbb{R}^{n}.$$