The Diagonal Sets of the Cauchy Product and Re-indexing of Diagonal Sums

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{N}$, $\mathbb{N}_{0}$ and their addition and order be as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let intervals $\{m,\dots,n\}$ and segments $[n]$ be as in Intervals of Natural Numbers (i) and Intervals of Natural Numbers (ii), let the difference $n-k$ of $k,n\in\mathbb{N}_{0}$ with $k\le n$ be as there, and let finite sums in $\mathbb{R}$ be as in Sums and Products over a Finite Set and over an Interval (iii), Sums and Products over a Finite Set and over an Interval (iv) and Sums and Products over a Finite Set and over an Interval (v). For $n\in\mathbb{N}_{0}$ let

$$D_{n}=\{(i,j)\in[n]\times[n]:i+j=n+1\},$$

a subset of the Cartesian product $[n]\times[n]$, a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), with $(i,j)$ the ordered pair. This is the set of Finite Sums of Reals: Congruence, the Product Map (x,y) ↦ f(x)h(y), and the Sequence of Diagonal Sums (iii), and for $n\in\mathbb{N}$ the set $D_{n}$ of The Cauchy Product of Two Absolutely Convergent Series.

(i) Let $n\in\mathbb{N}_{0}$ and let $q$ be a set. Then $q\in D_{n}$ if and only if $q=(i,j)$ for some $i,j\in[n]$ with $i+j=n+1$.

(ii) For every $n\in\mathbb{N}_{0}$, $D_{n}$ is a finite set and $D_{n}\subseteq\mathbb{N}\times\mathbb{N}$.

(iii) Let $m\in\mathbb{N}_{0}$. For every $k\in\{0,\dots,m\}$ the difference $m-k\in\mathbb{N}_{0}$ is defined and $(k+1,(m-k)+1)\in D_{m+1}$; there is exactly one map $\sigma:\{0,\dots,m\}\to D_{m+1}$ with $\sigma(k)=(k+1,(m-k)+1)$ for every $k\in\{0,\dots,m\}$, and $\sigma$ is a bijection.

(iv) Let $m\in\mathbb{N}_{0}$, let $E$ be a set with $D_{m+1}\subseteq E$ (for instance $E=\mathbb{N}\times\mathbb{N}$, by (ii)), and let $g:E\to\mathbb{R}$ be a map, $g(i,j)$ standing for $g((i,j))$. There is exactly one map $a:\{0,\dots,m\}\to\mathbb{R}$ with $a_{k}=g(k+1,(m-k)+1)$ for every $k\in\{0,\dots,m\}$, the argument lying in $D_{m+1}$ by (iii); and

$$\sum_{(i,j)\in D_{m+1}}g(i,j)=\sum_{k=0}^{m}a_{k}=\sum_{k=0}^{m}g(k+1,(m-k)+1).$$