Iterated Operations: Finite Sums and Finite Products

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $\ast$ be a binary operation on a set $X$, let $n\in\mathbb{N}$, and let $[n]$ be as in Intervals of Natural Numbers §segment.

¶ For a map $a:[n]\to X$, $k\mapsto a_{k}$, the iterated operation of $a$ is

$$\mathop{\ast}\limits_{k=1}^{n}a_{k}=s(n),$$

where $s$ is the map of Iterating a Binary Operation along a Finite List §existence for $\ast$ and $a$, and $n\in[n]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment; that is, $(\dots(a_{1}\ast a_{2})\ast\dots)\ast a_{n}$, also written $a_{1}\ast\dots\ast a_{n}$. For an expression $t(k)$ with $t(k)\in X$ for every $k\in[n]$, $\mathop{\ast}\limits_{k=1}^{n}t(k)$ is the iterated operation of the map $k\mapsto t(k)$ on $[n]$.

¶ For a map $a$ from a set containing $[n]$ to $X$, $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ denotes the iterated operation of $a|_{[n]}$.

¶ If $\ast$ is written $+$, the iterated operation is the finite sum $\sum_{k=1}^{n}a_{k}$; if $\ast$ is written $\cdot$, it is the finite product $\prod_{k=1}^{n}a_{k}$.