Kit for def:almost-sure-convergence

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; the element $0$ of $[0,\infty]$ is that of $\mathbb{R}$ (Addition and Multiplication on [0,∞] (ii)). Each parameter of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) other than its metric space is the first of these seventeen 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 seventeen variables as parameters.

(i) Almost sure convergence. 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 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$ almost surely" on $x_{0},\dots,x_{q-1}$ is predicative.