Proof of Kit for def:sequence-nbg

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{1}$ is distinct from $x_{0}$ also when $n=1$. Let $\nu$, $p$, $u$, $u'$, $v$ and $v'$ be pairwise distinct set variables, all distinct from $x_{0}$, $x_{1}$ and from $x_{0},\dots,x_{n-1}$; $\nu$ is the parameter $\mathbb{N}$ of the statement, its fixed value being the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii). By Sequences (i), a sequence in a set $X$ is a map $\mathbb{N}\to X$; both parts below use this.

Sequences. Let $\mu(F,A,B)$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), with $F=x_{0}$, $A=\nu$, $B=x_{1}$ and the set variables $p,u,u',v,v'$ above, so that these eight variables are pairwise distinct as that lemma requires; only $p,u,v,v'$ occur in $\mu$. The formula

$$\psi=\mu(x_{0},\nu,x_{1})$$

is predicative, its free variables are $x_{0}$, $\nu$ and $x_{1}$, and, under every assignment of sets to $x_{0}$ and $x_{1}$, it holds if and only if $x_{0}$ is a map $x_{0}:\mathbb{N}\to x_{1}$, that is, a sequence in $x_{1}$. So $\psi$ is a predicative formula in $x_{0},x_{1}$ with parameter $\mathbb{N}$.

Any positions. By Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=i$ and $\sigma(1)=j$, the formula $\psi(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is a sequence in $x_{j}$. This proves (i).

The class of sequences. For a set $X$, the class $S=X^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $X$ has as its elements exactly the maps $\mathbb{N}\to X$, that is, the sequences in $X$, which proves (ii) (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), as $\mathbb{N}$ is a set).