Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $\ast$ be an associative and commutative binary operation on a set $X$ with a neutral element $e$, and let iterated operations over finite sets and intervals be as in Sums and Products over a Finite Set and over an Interval §operation, Sums and Products over a Finite Set and over an Interval §empty, Sums and Products over a Finite Set and over an Interval §subsets and Sums and Products over a Finite Set and over an Interval §intervals. Let $A$ and $B$ be finite sets; singletons, $A\cup B$ and $A\times B$ are finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §small and Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §union.

¶ For every set $y$ and $f:\{y\}\to X$, $\mathop{\ast}\limits_{x\in\{y\}}f(x)=f(y)$.

¶ If $A\cap B=\emptyset$ and $f:A\cup B\to X$, then $\mathop{\ast}\limits_{x\in A\cup B}f(x)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in B}f(x)\Big)$.

¶ If $g:B\to A$ is a bijection and $f:A\to X$, then $\mathop{\ast}\limits_{y\in B}f(g(y))=\mathop{\ast}\limits_{x\in A}f(x)$.

¶ If $f:A\times B\to X$, then

$$\mathop{\ast}\limits_{(x,y)\in A\times B}f(x,y)=\mathop{\ast}\limits_{x\in A}\Big(\mathop{\ast}\limits_{y\in B}f(x,y)\Big)=\mathop{\ast}\limits_{y\in B}\Big(\mathop{\ast}\limits_{x\in A}f(x,y)\Big).$$

¶ If $f,g:A\to X$, then $\mathop{\ast}\limits_{x\in A}\big(f(x)\ast g(x)\big)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in A}g(x)\Big)$.

¶ Let $\diamond$ be an associative and commutative binary operation on a set $Y$ with a neutral element $e'$, and $\varphi:X\to Y$ a map with $\varphi(e)=e'$ and $\varphi(x\ast y)=\varphi(x)\diamond\varphi(y)$ for all $x,y\in X$. For $f:A\to X$, $\varphi\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)=\mathop{\diamond}\limits_{x\in A}\varphi(f(x))$.

¶ Let $m,n\in\mathbb{N}_{0}$ with $m\le n+1$, and let $a$ be a map from a set containing $\{m,\dots,n+1\}$ to $X$. Then $\mathop{\ast}\limits_{k=m}^{n+1}a_{k}=\Big(\mathop{\ast}\limits_{k=m}^{n}a_{k}\Big)\ast a_{n+1}$.

¶ Let $m,n,p\in\mathbb{N}_{0}$, and let $a$ be a map from a set containing $\{m+p,\dots,n+p\}$ to $X$. Then $\mathop{\ast}\limits_{k=m}^{n}a_{k+p}=\mathop{\ast}\limits_{k=m+p}^{n+p}a_{k}$.