Extraction of a Term from a Finite Sum or Product in a Field

Let $K$ be a field. Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, ordered by the relations of Order on the Natural Numbers, and for $p\in\mathbb{N}$ let $[p]$ be the initial segment determined by $p$. Let $n\in\mathbb{N}$, let $a:[S(n)]\to K$ be a map with values written $a_{k}$, and let $j\in[S(n)]$. Sums and products below are the finite sums and the finite products of $K$.

Define the gap map $g_{j}:[n]\to[S(n)]$ by

Exactly one of the two cases applies to each $k\in[n]$, since the order on $\mathbb{N}$ is total, and the values lie in $[S(n)]$, since $k\le n$ implies both $k\le S(n)$ and $S(k)\le S(n)$; these order facts are those of Properties of the Order on the Natural Numbers.

Then the following hold.

1. (Gap map) $g_{j}$ is a bijection from $[n]$ onto the set of those $l\in[S(n)]$ with $l\ne j$.

2. (Sums)

3. (Products)