Let $\mathbb{R}^N$ be a D5630: Set of euclidean real numbers.
The dot product operation on $\mathbb{R}^N$ is the D4364: Real function \begin{equation} \mathbb{R}^N \times \mathbb{R}^N \to \mathbb{R}, \quad (x, y) \mapsto \sum_{n = 1}^N x_n y_n \end{equation}