Existence and Uniqueness of Iterates of a Binary Operation

Let $X$ be a set and let $\ast$ be a binary operation on $X$, that is, a map $\ast:X\times X\to X$, whose value at $(x,y)$ is written $x\ast y$. Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, let $n\in\mathbb{N}$, let $[n]$ be the initial segment determined by $n$, and let $a:[n]\to X$ be a map, whose value at $k$ is written $a_{k}$.

Then there is exactly one map $\sigma:[n]\to X$ such that

and

(Here $1\in[n]$ and, whenever $S(m)\in[n]$, also $m\in[n]$, by Basic Properties of Initial Segments of the Natural Numbers and Properties of the Order on the Natural Numbers, so both displayed conditions are meaningful.)