Properties of Finite Products

Let $K$ be a field, with additive identity $0$ and multiplicative identity $1$. 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, let $n\in\mathbb{N}$, and let $[n]$ be the initial segment determined by $n$. Let $a:[n]\to K$ and $b:[n]\to K$ be maps, with values written $a_{k}$ and $b_{k}$. All products below are the finite products of that definition.

Two different order relations occur below. In index ranges such as $1\le k\le n$ the symbol $\le$ is the order on $\mathbb{N}$ just cited; in claim 5 it is the order of the ordered field of real numbers. Then the following hold.

1. (Restriction and recursion) If $j\in[n]$ and $a'$ denotes the restriction of $a$ to $[j]$, then

Moreover

2. (Multiplicativity)

3. (A single factor different from the unit) Let $i\in[n]$ and suppose that $a_{k}=1$ for every $k\in[n]$ with $k\ne i$. Then

4. (Vanishing) $\prod_{k=1}^{n}a_{k}=0$ if and only if $a_{i}=0$ for some $i\in[n]$.

5. (Nonnegative factors) Suppose $K$ is the field of real numbers, with the order $\le$ of its ordered field structure, and that $0\le a_{k}$ for every $k\in[n]$. Then

and if in addition $a_{k}\le b_{k}$ for every $k\in[n]$, then