Kit for def:complex-exponential

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{N}$ and its element $1$, the addition of $\mathbb{N}_{0}$, the set $\mathbb{C}$ of complex numbers with its sum and product operations of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii) and its unit $1$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii)), the distance $d_{\mathbb{C}}$ on $\mathbb{C}$, and $\mathbb{R}$ with its order $\le$, its strict order $<$, its addition $+$ and its element $0$ are parameters. The complex exponential function is the map $\exp:\mathbb{C}\to\mathbb{C}$ of The Complex Exponential Function (i).

(i) The exponential. The condition "$x_{i}$ is the complex exponential function" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) A class for the exponential. There is a class $E$ such that, for every class $a$, $a\in E$ if and only if $a$ is the complex exponential function.