Proof of Reversal of a Finite Sum

Each result cited is universally quantified over the data in its own statement. Throughout, $S$ is the successor map of Natural Numbers, so that $N+1=S(N)$.

Claim 1. Let $a\in[N]$, so that $a\le N$, which by Order on the Natural Numbers means $a<N$ or $a=N$.

Existence and uniqueness of $k$. We first show $a<N+1$. One has $N<S(N)=N+1$ by claim 5 of Properties of the Order on the Natural Numbers. If $a=N$ this is $a<N+1$. If $a<N$, then $a<N$ and $N<N+1$ give $a<N+1$ by the transitivity of $<$ in claim 1 of Properties of the Order on the Natural Numbers. Hence, by claim 7 of Properties of the Order on the Natural Numbers applied with $m=a$ and $y=N+1$, there is exactly one $k\in\mathbb{N}$ with $N+1=a+k$.

The number $k$ lies in $[N]$. By claim 4 of Arithmetic of Addition on the Natural Numbers, $k+a=a+k=N+1=S(N)$, and $k<k+a$ by claim 6 of Properties of the Order on the Natural Numbers; so $k<S(N)$. Hence $k\le S(N)$ by claim 1 of Properties of the Order on the Natural Numbers, and $k\ne S(N)$, since $k=S(N)$ would give $k<k$, which is excluded by claim 2 of that lemma. Therefore $k\le N$ by claim 5 of Properties of the Order on the Natural Numbers, that is, $k\in[N]$. This defines the map $\sigma_{N}:[N]\to[N]$.

Involution. Let $a\in[N]$ and put $k=\sigma_{N}(a)$, so that $a+k=N+1$. By definition $\sigma_{N}(k)$ is the unique $k'\in\mathbb{N}$ with $k+k'=N+1$. Since $k+a=a+k=N+1$ by claim 4 of Arithmetic of Addition on the Natural Numbers, uniqueness gives $k'=a$, that is, $\sigma_{N}(\sigma_{N}(a))=a$.

Bijection. Let $b\in[N]$. The element $a=\sigma_{N}(b)$ of $[N]$ satisfies $\sigma_{N}(a)=\sigma_{N}(\sigma_{N}(b))=b$. If $a'\in[N]$ also satisfies $\sigma_{N}(a')=b$, then $a'=\sigma_{N}(\sigma_{N}(a'))=\sigma_{N}(b)=a$. Thus for every $b\in[N]$ there is exactly one $a\in[N]$ with $\sigma_{N}(a)=b$, which is the defining property of a bijection in Bijection of Sets.

The reading in an ordered field. Let $F$ be an ordered field with canonical map $\iota_{F}$, let $a\in[N]$ and $k=\sigma_{N}(a)$. By claim 4 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, $\iota_{F}(a)+\iota_{F}(k)=\iota_{F}(a+k)=\iota_{F}(N+1)$, and $\iota_{F}(N+1)=\iota_{F}(N)+1$ by claim 1 of that lemma. Adding $-\iota_{F}(a)$ to both sides gives $\iota_{F}(k)=\iota_{F}(N)+1-\iota_{F}(a)$.

Claim 2. By claim 1, $\sigma_{N}$ is a bijection from $[N]$ to $[N]$, so claim 1 of Invariance of Finite Sums and Products under Reindexing by a Permutation, applied to the map $h$ and the bijection $\sigma_{N}$, gives $\sum_{a=1}^{N}h_{\sigma_{N}(a)}=\sum_{a=1}^{N}h_{a}$.