Kit for def:random-element-law-metric

In the setting of Measurable Functions and the Lebesgue Integral: Standing Notation and 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,j,k,l,m,p,q,r,s,t<N$, not necessarily distinct. Let $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$ and $Q$ be distinct class variables with the values of the class variables $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) (its $P$ being written $\oplus$ and its $N$ being written $\mathbb{N}$ here), and let $\infty$, $0$ and $1$ be distinct set variables, other than $x_{0},\dots,x_{N-1}$, whose values are the element $\infty$ of The Extended Real Line, Its Order, and [0,∞] (i) and the elements $0$ and $1$ of $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)). Let $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$, $\mathcal{B}(\mathbb{R})$ and $\mathcal{B}([0,\infty])$ be further distinct class variables with values, in this order, the set of real numbers, its order, its strict order, its addition, its zero, the Borel $\sigma$-algebra of Borel Sigma-Algebra of a Metric Space (ii) and the Borel $\sigma$-algebra of The Borel σ-Algebra of [0,∞] (ii). A condition on $x_{0},\dots,x_{N-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these seventeen variables as parameters.

(i) Identically distributed random elements. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $\Omega'=x_{l}$, $\mathcal{F}'=x_{m}$, $P'=x_{p}$, $S=x_{q}$, $d=x_{r}$, $X=x_{s}$ and $Y=x_{t}$, the condition "$(\Omega,\mathcal{F})$ and $(\Omega',\mathcal{F}')$ are measurable spaces, $P$ is a measure on $(\Omega,\mathcal{F})$ and $P'$ a measure on $(\Omega',\mathcal{F}')$, $(\Omega,\mathcal{F},P)$ and $(\Omega',\mathcal{F}',P')$ are probability spaces, $d$ is a map from the Cartesian product $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, $X$ is a random element of $S$ on $(\Omega,\mathcal{F},P)$, $Y$ is a random element of $S$ on $(\Omega',\mathcal{F}',P')$, and $X$ and $Y$ are identically distributed" is predicative.