Kit for def:series-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. A condition on $x_{0},\dots,x_{n-1}$ is predicative if it is 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}$, $\mathbb{R}$, the operations $+$ and $\cdot$, the order $\le$, the strict order $<$ and the elements $0$ and $1$ of $\mathbb{R}$, the distance $d_{\mathbb{R}}$ on $\mathbb{R}$, the addition of $\mathbb{N}_{0}$ and the element $1$ of $\mathbb{N}$ are parameters. Sequences are as in Sequences (i), $|x|$ is the absolute value of $x\in\mathbb{R}$, and the sequence of partial sums, convergence and divergence of a series, and absolute convergence are as in Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (i), Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii) and Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (iii).

(i) Partial sums. The condition "$x_{i}$ and $x_{j}$ are sequences in $\mathbb{R}$, and $x_{j}$ is the sequence of partial sums of $x_{i}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Absolute values. The condition "$x_{i}$ and $x_{j}$ are sequences in $\mathbb{R}$, and $x_{j}(k)=|x_{i}(k)|$ for every $k\in\mathbb{N}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) Convergent series. The condition "$x_{i}$ is a sequence in $\mathbb{R}$ and its series converges" on $x_{0},\dots,x_{n-1}$ is predicative.

(iv) Divergent series. The condition "$x_{i}$ is a sequence in $\mathbb{R}$ and its series diverges" on $x_{0},\dots,x_{n-1}$ is predicative.

(v) Absolutely convergent series. The condition "$x_{i}$ is a sequence in $\mathbb{R}$ and its series converges absolutely" on $x_{0},\dots,x_{n-1}$ is predicative.

(vi) The class of convergent series. There is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a sequence in $\mathbb{R}$ whose series converges.

(vii) The class of divergent series. There is a class $D$ such that, for every class $a$, $a\in D$ if and only if $a$ is a sequence in $\mathbb{R}$ whose series diverges.

(viii) The class of absolutely convergent series. There is a class $A$ such that, for every class $a$, $a\in A$ if and only if $a$ is a sequence in $\mathbb{R}$ whose series converges absolutely.