The Dot Product 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}$, and let $x,y\in\mathbb{R}^{n}$, Euclidean space, with components as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership.

¶ The dot product of $x$ and $y$ is the real number

$$x\cdot y=\sum_{k=1}^{n}x_{k}y_{k},$$

the sum of the pointwise product $xy\in\mathbb{R}^{[n]}$, $k\mapsto x_{k}y_{k}$; it lies in $\mathbb{R}$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set §segment-sums.