Proof of The Map of Consecutive Differences of a Finite List of Reals Exists, and Its Sum Telescopes

For $k\in[n]$, $k+1\in[n+1]$ and $k\in[n+1]$ (as $[n]\subseteq[n+1]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (ii)), so $d(k+1)\in\mathbb{R}$, $d(k)\in\mathbb{R}$ and $d(k+1)-d(k)\in\mathbb{R}$. Hence the map $g:[n]\to\mathbb{R}$, $k\mapsto d(k+1)-d(k)$, of Sets and Maps: Ordinary Notation (v) has $g(k)=d(k+1)-d(k)$ for every $k\in[n]$; and every map $g':[n]\to\mathbb{R}$ with this property satisfies $g'(k)=g(k)$ for every $k\in[n]$, so $g'=g$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

$\mathbb{R}$, with $+$, $\cdot$, $0$ and $1$, is an ordered field by The Real Line: Standing Notation and Background for Calculus on Intervals (ii), hence a field and so a commutative ring by Ordered Fields (i) and Fields (i). By Iterated Operations: Finite Sums and Finite Products (i), the sum $\sum_{k=1}^{n}(d_{k+1}-d_{k})$, with $d_{k}=d(k)$, is the iterated sum of the map $k\mapsto d(k+1)-d(k)$ on $[n]$, which is $g$; so $\sum_{k=1}^{n}g(k)=\sum_{k=1}^{n}(d_{k+1}-d_{k})=d_{n+1}-d_{1}$ by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality (iii), applied with $R=\mathbb{R}$. That is, $\sum_{k=1}^{n}g(k)=d(n+1)-d(1)$.