Kit for def:holomorphic-function

In the setting of Complex Analysis: Standing Notation; this item is a statement of the metatheory. Let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$, not necessarily distinct. The first clause 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 of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. The set $\mathbb{C}$ with its sum and product operations, the distance $d_{\mathbb{C}}$, and $\mathbb{R}$ with its addition $+$, its element $0$, its order $\le$ and the strict order $<$ of $\le$ are parameters. Subsets are as in Subclasses and Subsets (i), maps as in Functions, Values of a Function, and Functions from One Class to Another (iii), and open subsets of $(\mathbb{C},d_{\mathbb{C}})$ as in Open Subset of a Metric Space (i).

(i) Holomorphic functions. With $U=x_{i}$, $f=x_{j}$ and $W=x_{k}$, the condition "$U\subseteq\mathbb{C}$ and $U$ is open in $(\mathbb{C},d_{\mathbb{C}})$, $f$ is a map $f:U\to\mathbb{C}$, $W\subseteq U$, $W$ is open in $(\mathbb{C},d_{\mathbb{C}})$, and $f$ is holomorphic on $W$" is predicative.

(ii) The class of holomorphic functions. For every open subset $U$ of $(\mathbb{C},d_{\mathbb{C}})$ and every open subset $W$ of $(\mathbb{C},d_{\mathbb{C}})$ with $W\subseteq U$ there is a class $H$ such that, for every class $f$, $f\in H$ if and only if $f$ is a map $f:U\to\mathbb{C}$ that is holomorphic on $W$.