let Omega be non empty finite set ; :: thesis: for f being Function of Omega,REAL holds f is Real-Valued-Random-Variable of (Trivial-SigmaField Omega)
let f be Function of Omega,REAL; :: thesis: f is Real-Valued-Random-Variable of (Trivial-SigmaField Omega)
set Sigma = Trivial-SigmaField Omega;
consider X being Element of Trivial-SigmaField Omega such that
A1: ( dom f = X & f is X -measurable ) by Th8;
A2: ( f is X -measurable & dom f = Omega ) by FUNCT_2:def 1, A1;
X = [#] (Trivial-SigmaField Omega) by A1, A2;
hence f is Real-Valued-Random-Variable of (Trivial-SigmaField Omega) by A1; :: thesis: verum