Finite Sums of Reals: Congruence, the Product Map (x,y) ↦ f(x)h(y), and the Sequence of Diagonal Sums

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, finite sums in $\mathbb{R}$ are as in Sums and Products over a Finite Set and over an Interval (iii) and Sums and Products over a Finite Set and over an Interval (v), and $[n]$ is as in Intervals of Natural Numbers (ii).

(i) Let $A$ be a finite set, and let $f:D\to\mathbb{R}$ and $f':D'\to\mathbb{R}$ be maps on sets $D$ and $D'$ containing $A$ with $f(x)=f'(x)$ for every $x\in A$. Then $\sum_{x\in A}f(x)=\sum_{x\in A}f'(x)$.

(ii) Let $A$ and $B$ be sets and let $f:A\to\mathbb{R}$ and $h:B\to\mathbb{R}$ be maps. There is exactly one map $m:A\times B\to\mathbb{R}$ with $m(x,y)=f(x)\,h(y)$ for all $x\in A$ and $y\in B$.

(iii) Let $(a_{k})$ and $(b_{k})$ be sequences in $\mathbb{R}$. There is a sequence $(c_{n})$ in $\mathbb{R}$ with

$$c_{n}=\sum_{(i,j)\in[n]\times[n],\,i+j=n+1}a_{i}b_{j}\qquad(n\in\mathbb{N}),$$

the sum being that over the set $\{(i,j)\in[n]\times[n]:i+j=n+1\}$, which is finite, of the map $\mathbb{N}\times\mathbb{N}\to\mathbb{R}$, $(i,j)\mapsto a_{i}b_{j}$, of (ii).