Finite Product Notation in a Field

Let $K$ be a field, let $n$ be a natural number with successor map $S$ as in that definition, let $[n]$ be the initial segment determined by $n$, and let $a:[n]\to K$ be a map, whose value at $k$ is written $a_{k}$.

Let $\pi:[n]\to K$ be the map given by Existence and Uniqueness of Iterates of a Binary Operation for the multiplication of $K$, that is, the unique map $[n]\to K$ with

$$\pi(1)=a_{1},\qquad \pi(S(m))=\pi(m)\,a_{S(m)}\quad\text{whenever }S(m)\in[n].$$

For $j\in[n]$ the finite product of $a_{1},\dots,a_{j}$ is

$$\prod_{k=1}^{j}a_{k}=\pi(j).$$