Kit for def:complex-numbers-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<n$. 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{R}$, its operations $+$ and $\cdot$, and its element $0$ are parameters. The sum operation and the product operation of the set $\mathbb{C}$ of complex numbers are the binary operations on $\mathbb{C}$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii).

(i) The sum. The condition "$x_{i}$ is the sum operation of $\mathbb{C}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) The product. The condition "$x_{i}$ is the product operation of $\mathbb{C}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) A class for the sum. There is a class $A$ such that, for every class $a$, $a\in A$ if and only if $a$ is the sum operation of $\mathbb{C}$.

(iv) A class for the product. There is a class $M$ such that, for every class $a$, $a\in M$ if and only if $a$ is the product operation of $\mathbb{C}$.