Kit for def:sine-cosine-real

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$. Each of the first two clauses states that a condition 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}$ 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), its unit $1$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii)) and its imaginary unit, the map $\mathbb{R}\to\mathbb{C}$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), 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. In every clause, the cosine function and the sine function are the cosine $\cos:\mathbb{R}\to\mathbb{R}$ and the sine $\sin:\mathbb{R}\to\mathbb{R}$.

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

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

(iii) A class for the cosine. There is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is the cosine function.

(iv) A class for the sine. There is a class $S$ such that, for every class $a$, $a\in S$ if and only if $a$ is the sine function.