Proof of Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n

Each result cited is universally quantified over the data in its own statement.

Clause naturals. $\mathbb{N}\subseteq\mathbb{N}_{0}$ is stated in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, and by Subclasses and Subsets §subclass it means that $n\in\mathbb{N}_{0}$ for every $n\in\mathbb{N}$.

Clause one. $1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one, and then $1\in\mathbb{N}_{0}$ by the clause naturals.

The set $[n]$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n]=\{k\in\mathbb{N}:k\le n\}$. By Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one, $1\in\mathbb{N}$ and, as $n\in\mathbb{N}$, $1\le n$; so $1\in[n]$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, and $[n]\neq\emptyset$. Further, $[n]$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals, since $[n]=\{1,\dots,n\}$ is an interval by Intervals of Natural Numbers §segment, and $\#[n]=n$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §intervals. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, the identity $\mathrm{id}_{[n]}$ is a bijective map from $[n]=[\#[n]]$ onto $[n]$ with $\mathrm{id}_{[n]}(k)=k$ for every $k\in[n]$.

Clause iterated-segment. Sums and Products over a Finite Set and over an Interval §operation, applied with $A=[n]$, which is finite and nonempty, $f=a$ and the bijection $\varphi=\mathrm{id}_{[n]}$, gives

$$\mathop{\ast}\limits_{k\in[n]}a_{k}=\mathop{\ast}\limits_{k=1}^{n}a(\mathrm{id}_{[n]}(k)),$$

where by Iterated Operations: Finite Sums and Finite Products §iterated the right side is the iterated operation of the map $k\mapsto a(\mathrm{id}_{[n]}(k))$ on $[n]$. This map and $a$ are functions with domain $[n]$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $a(\mathrm{id}_{[n]}(k))=a(k)$ for every $k\in[n]$ since $\mathrm{id}_{[n]}(k)=k$; so the map is $a$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Hence the right side is the iterated operation $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ of $a$ of Iterated Operations: Finite Sums and Finite Products §iterated, which proves the clause.

Clause interval-segment. We have $1\in\mathbb{N}_{0}$ by the clause one, $n\in\mathbb{N}_{0}$ by the clause naturals, and $1\le n$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one; and $a$ is a map from $[n]=\{1,\dots,n\}$ to $X$, by Intervals of Natural Numbers §segment. So Sums and Products over a Finite Set and over an Interval §intervals applies with $m=1$ and gives, in its reading, $\mathop{\ast}\limits_{k=1}^{n}a_{k}=\mathop{\ast}\limits_{k\in\{1,\dots,n\}}a_{k}$, which is $\mathop{\ast}\limits_{k\in[n]}a_{k}$ as $\{1,\dots,n\}=[n]$. Here $a$ is a map from a set containing $[n]$, and $[n]\neq\emptyset$ by the paragraph on $[n]$, so by Sums and Products over a Finite Set and over an Interval §subsets this denotes the iterated operation of $a|_{[n]}$ over the finite set $[n]$; and $a|_{[n]}=a$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §restriction. So it is the iterated operation $\mathop{\ast}\limits_{k\in[n]}a_{k}$ of $a$ of Sums and Products over a Finite Set and over an Interval §operation, which proves the clause.

Clause readings. Read as in Iterated Operations: Finite Sums and Finite Products §iterated, the equation is the clause iterated-segment; read as in Sums and Products over a Finite Set and over an Interval §intervals, it is the clause interval-segment.