Proof of Iterating a Binary Operation along a Finite List

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

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$ is the least natural number by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, $1\le n$, so $1\in[n]$; and $n\in[n]$, as $n\le 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. For $k\in\mathbb{N}$ let $S_{k}=\{j\in[n]:k+1\le j\ \text{or}\ j=n\}$, a subset of $[n]$, hence of $\mathbb{N}_{0}$. It contains $n$, since $n\in[n]$; as the order is a well-order on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, $S_{k}$ has a least element, so $c_{k}=\min S_{k}$, formed in $\mathbb{N}_{0}$ as in Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least, is defined, and $c_{k}\in S_{k}\subseteq[n]$. Hence $u\ast a_{c_{k}}\in X$ for all $k\in\mathbb{N}$ and $u\in X$, an expression in which the defined set symbols $\min$, the value of $a$ and the value of $\ast$ are used properly, and by Maps and Relations Given by Formulas §binary there is a map $g:\mathbb{N}\times X\to X$ with $g(k,u)=u\ast a_{c_{k}}$ for all $k\in\mathbb{N}$ and $u\in X$. If $k<n$, then $c_{k}=k+1$: by Indices $k+1\in[n]$, and $k+1\le k+1$, so $k+1\in S_{k}$; and every $j\in S_{k}$ satisfies $k+1\le j$, directly or, when $j=n$, because $k+1\le n$ by Indices; so $k+1$ is a least element of $S_{k}$, and it equals $c_{k}$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §least-unique. Thus $g(k,u)=u\ast a_{k+1}$ for all $k\in\mathbb{N}$ with $k<n$ and all $u\in X$. By Recursion on the Natural Numbers Starting at One §recursion, as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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]}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $s$ is a function with domain $[n]\cap\mathbb{N}=[n]$ and values $s(k)=f(k)\in X$ for $k\in[n]$, so $s:[n]\to X$ is a map by Functions, Values of a Function, and Functions from One Class to Another §map. 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 induction from $1$ on $\mathbb{N}$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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.