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

Each result cited is universally quantified over the data in its own statement.

The operations involved. Let $b:[n]\to X$, $b(j)=a_{m+j}$, be the map of the statement, and let $p$ be any of $m+n$, $m$ and $n$; then $p\in\mathbb{N}$ by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §sum, and $[p]$ is finite (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 §naturals) and nonempty. By Sums and Products over a Finite Set and over an Interval §subsets, $\mathop{\ast}\limits_{k\in[m]}a_{k}$ is the operation over $[m]$ of $a|_{[m]}$, and $\mathop{\ast}\limits_{j\in[n]}a_{m+j}$ is that over $[n]$ of $b$.

The two readings. The equalities

$$\mathop{\ast}\limits_{k=1}^{m+n}a_{k}=\mathop{\ast}\limits_{k\in[m+n]}a_{k},\qquad\mathop{\ast}\limits_{k=1}^{m}a_{k}=\mathop{\ast}\limits_{k\in[m]}a_{k},\qquad\mathop{\ast}\limits_{j=1}^{n}a_{m+j}=\mathop{\ast}\limits_{j\in[n]}a_{m+j}\tag{1}$$

hold with the left sides read in either sense. In the sense of Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction, the left sides are the iterated operations of $a$, $a|_{[m]}$ and $b$, and (1) holds for these three maps by the indices clause of the setting. In the sense of Sums and Products over a Finite Set and over an Interval §intervals, with lower index $1$ and upper index $p$, the left sides are the operations over $\{1,\dots,p\}=[p]$ of $a$ (for $p=m+n$ and $p=m$, as $[m]\subseteq[m+n]$) and of $b$ (for $p=n$), which is (1).

Clause split. As $\ast$ is associative, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §splitting, with its $n$ and $m$ taken to be our $m$ and $n$, gives

$$\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)$$

in the reading of Iterated Operations: Finite Sums and Finite Products §iterated. Replacing each of the three iterated operations by the operation over a segment that equals it by (1) gives the clause.

Clause interval-split. By (1), each of the three operations from $1$, in either reading, equals the corresponding operation over $[m+n]$, $[m]$ or $[n]$ in the clause split; this is the last assertion of the clause. Substituting these equalities into the clause split, for any choice of readings, gives the displayed identity.