ℝⁿ Is a Real Vector Space

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\in\mathbb{N}$, and let Euclidean space $\mathbb{R}^{n}$ carry the sum and the scalar multiple of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv).

(i) $\mathbb{R}^{n}$ is a real vector space. $\mathbb{R}^{n}$, with this addition and scalar multiplication, is a real vector space. Its zero vector is the origin $0=(0,\dots,0)$, and the negative of $x\in\mathbb{R}^{n}$ is the componentwise negative $-x=(-x_{1},\dots,-x_{n})$ of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv).