Splitting an Operation over the Segment [m+n] into [m] and a Shifted Copy of [n]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\ast$ be an associative and commutative binary operation on a set $X$, let $m,n\in\mathbb{N}$, with $+$ as in Arithmetic and Order of the Natural Numbers and segments $[p]$ as in Intervals of Natural Numbers §segment; here $[m+n]$ is defined since $m+n\in\mathbb{N}$, and $[m]\subseteq[m+n]$, by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §sum. Let $a:[m+n]\to X$, $k\mapsto a_{k}$, be a map. As $m+j\in[m+n]$ for every $j\in[n]$ by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §shift, there is a map $b:[n]\to X$ with $b(j)=a_{m+j}$, and the operation over $[n]$ of $j\mapsto a_{m+j}$ is that of $b$. Operations over the finite sets $[m+n]$, $[m]$ and $[n]$ are as in Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §subsets; in particular $\mathop{\ast}\limits_{k\in[m]}a_{k}$ is the operation over $[m]$ of the restriction $a|_{[m]}$.

¶ The operation over $[m+n]$ splits as

$$\mathop{\ast}\limits_{k\in[m+n]}a_{k}=\Big(\mathop{\ast}\limits_{k\in[m]}a_{k}\Big)\ast\Big(\mathop{\ast}\limits_{j\in[n]}a_{m+j}\Big).$$

¶ The operations from $1$ split in the same way:

$$\mathop{\ast}\limits_{k=1}^{m+n}a_{k}=\Big(\mathop{\ast}\limits_{k=1}^{m}a_{k}\Big)\ast\Big(\mathop{\ast}\limits_{j=1}^{n}a_{m+j}\Big),$$

where each of the three operations from $1$ may be read, independently of the other two, either as in Sums and Products over a Finite Set and over an Interval §intervals or as in Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction; in every reading each of them equals the corresponding operation over $[m+n]$, $[m]$ or $[n]$ in the clause split.