Kit for def:convergence-modes

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, let $q\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{q-1}$ be distinct set variables, and let $i_{0},\dots,i_{6}<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, and let $\cdot_{\mathbb{R}}$ and $d_{\mathbb{R}}$ be further distinct class variables with values the multiplication of $\mathbb{R}$ and the distance on $\mathbb{R}$; the elements $0$ and $1$ of $[0,\infty]$ are those of $\mathbb{R}$ (Addition and Multiplication on [0,∞] (ii)). Each parameter of Kit for def:separable-metric (i), and of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) for the metric space $(\mathbb{R},d_{\mathbb{R}})$, is the first of these nineteen variables with its value. 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 these nineteen variables as parameters.

(i) Convergence in probability. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$, $S=x_{i_{3}}$, $d=x_{i_{4}}$, $(X_{n})=x_{i_{5}}$ and $X=x_{i_{6}}$, the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $(S,d)$ is a separable metric space, $(X_{n})$ is a sequence of random elements of $S$, $X$ is a random element of $S$, and $(X_{n})$ converges to $X$ in probability" on $x_{0},\dots,x_{q-1}$ is predicative.