Finite Sums of the Coordinates of a Point of ℝⁿ

In the settings of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Euclidean Space and Real Matrices: Standing Notation, let $N\in\mathbb{N}$. For a point $t$ of Euclidean space, $t_{k}$ is its $k$-th component; $\sum_{k=1}^{N}t_{k}$ is the finite sum of Iterated Operations: Finite Sums and Finite Products (iii), formed with the addition of $\mathbb{R}$; and $t|_{[N]}$ is the restriction of $t$ to $[N]$.

(i) For $t\in\mathbb{R}^{N+1}$: $t|_{[N]}\in\mathbb{R}^{N}$, and $(t|_{[N]})_{k}=t_{k}$ for every $k\in[N]$.

(ii) For $t\in\mathbb{R}^{1}$: $\sum_{k=1}^{1}t_{k}=t_{1}$.

(iii) For $t\in\mathbb{R}^{N+1}$:

$$\sum_{k=1}^{N+1}t_{k}=\sum_{k=1}^{N}(t|_{[N]})_{k}+t_{N+1}.$$

(iv) For $t\in\mathbb{R}^{N}$: $\sum_{k=1}^{N}t_{k}\in\mathbb{R}$.

(v) For $\tau\in\mathbb{R}^{N}$ and $c\in\mathbb{R}$:

$$c\sum_{k=1}^{N}\tau_{k}=\sum_{k=1}^{N}(c\tau)_{k}.$$

(vi) For $t\in\mathbb{R}^{N}$ with $0\le t_{k}$ for every $k\in[N]$: $t_{j}\le\sum_{k=1}^{N}t_{k}$ for every $j\in[N]$, and $0\le\sum_{k=1}^{N}t_{k}$.