Proof of Iterating a Binary Operation along a Finite List

Indices. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n]=\{k\in\mathbb{N}:k\le n\}$. Since $1\le n$ by Arithmetic and Order of the Natural Numbers §least, $1\in[n]$. Let $k\in\mathbb{N}$ with $k<n$. Then $k+1\le n$: otherwise $n<k+1$ by Arithmetic and Order of the Natural Numbers §trichotomy and Arithmetic and Order of the Natural Numbers §partial-order, and $k<n<k+1$ contradicts Arithmetic and Order of the Natural Numbers §successor. So $k+1\in[n]$, and $a_{k+1}$ is defined.

Existence. Let $g:\mathbb{N}\times X\to X$ be given by $g(k,u)=u\ast a_{k+1}$ if $k<n$ and $g(k,u)=u$ otherwise, a map by Maps and Relations Given by Formulas §binary. By Recursion on the Natural Numbers Starting at One §recursion, applied with the set $X$, the element $a_{1}$ and the map $g$, there is a map $f:\mathbb{N}\to X$ with $f(1)=a_{1}$ and $f(k+1)=g(k,f(k))$ for every $k\in\mathbb{N}$. Let $s=f|_{[n]}:[n]\to X$. Then $s(1)=f(1)=a_{1}$, and for $k\in[n]$ with $k<n$ we have $k+1\in[n]$, so

$$s(k+1)=f(k+1)=g(k,f(k))=f(k)\ast a_{k+1}=s(k)\ast a_{k+1}.$$

Uniqueness. Let $s,s':[n]\to X$ both have the stated properties, and let $A$ be the set of $k\in\mathbb{N}$ such that either $n<k$, or $k\le n$ and $s(k)=s'(k)$. Then $1\in A$, since $1\le n$ and $s(1)=a_{1}=s'(1)$. Let $k\in A$. If $n<k+1$, then $k+1\in A$. Otherwise $k+1\le n$ by Arithmetic and Order of the Natural Numbers §trichotomy, and since $k<k+1$ by Arithmetic and Order of the Natural Numbers §successor, Arithmetic and Order of the Natural Numbers §partial-order gives $k<n$; in particular $n<k$ fails by trichotomy, so $s(k)=s'(k)$ because $k\in A$, and

$$s(k+1)=s(k)\ast a_{k+1}=s'(k)\ast a_{k+1}=s'(k+1),$$

so again $k+1\in A$. By Arithmetic and Order of the Natural Numbers §induction, $A=\mathbb{N}$. For $k\in[n]$ we have $k\le n$, so $n<k$ fails by trichotomy, and $k\in A$ gives $s(k)=s'(k)$. Hence $s=s'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.