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;
( ex X being Element of Trivial-SigmaField Omega st
( dom f = X & f is_measurable_on X ) & dom f = Omega ) by Th8, FUNCT_2:def 1;
hence f is Real-Valued-Random-Variable of Trivial-SigmaField Omega by Def2; :: thesis: verum