Kit for def:sequence-nbg

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j<n$, not necessarily distinct.

(i) Sequences. The condition "$x_{i}$ is a sequence in $x_{j}$" on $x_{0},\dots,x_{n-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}$ is a parameter.

(ii) The class of sequences. For every set $X$ there is a class $S$ such that, for every class $a$, $a\in S$ if and only if $a$ is a sequence in $X$.