Kit for def:convergence-in-distribution-metric

In the setting of Measurable Functions and the Lebesgue Integral: Standing Notation and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $q\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{q-1}$ be distinct set variables, and let $i_{0},\dots,i_{9}<q$, not necessarily distinct. Let $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$, $1$, $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$, $\mathcal{B}(\mathbb{R})$ and $\mathcal{B}([0,\infty])$ be the seventeen parameters of Kit for def:probability-space-random-variable (iv), other than $x_{0},\dots,x_{q-1}$, each with its kind and value there. Of the parameters of Kit for def:weak-convergence-measures-metric (i), its $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$ are $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$; its $\mathbb{R}$, $\le$, $<$, $+$ and $\mathcal{B}(\mathbb{R})$ are $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$ and $\mathcal{B}(\mathbb{R})$; and its other parameters, its $\cdot$, $d_{\mathbb{R}}$ and $\iota$ among them, are further distinct class variables, other than those above, with their values there. A condition on $x_{0},\dots,x_{q-1}$ is predicative if it is expressed by a predicative formula with $x_{0},\dots,x_{q-1}$ as the set variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and the seventeen variables above and the further variables as parameters.

(i) Convergence in distribution. With $S=x_{i_{0}}$, $d=x_{i_{1}}$, $(\Omega_{n})=x_{i_{2}}$, $(\mathcal{F}_{n})=x_{i_{3}}$, $(P_{n})=x_{i_{4}}$, $(X_{n})=x_{i_{5}}$, $\Omega=x_{i_{6}}$, $\mathcal{F}=x_{i_{7}}$, $P=x_{i_{8}}$ and $X=x_{i_{9}}$, and with $\Omega_{n}$, $\mathcal{F}_{n}$, $P_{n}$ and $X_{n}$ the values at $n$, the condition "$(S,d)$ is a metric space, $(\Omega_{n})$, $(\mathcal{F}_{n})$, $(P_{n})$ and $(X_{n})$ are functions with domain $\mathbb{N}$, for every $n\in\mathbb{N}$ the triple $(\Omega_{n},\mathcal{F}_{n},P_{n})$ is a probability space and $X_{n}$ is a random element of $S$ on it, $(\Omega,\mathcal{F},P)$ is a probability space and $X$ is a random element of $S$ on it, and $(X_{n})$ converges to $X$ in distribution" on $x_{0},\dots,x_{q-1}$ is predicative.