let Omega be non empty set ; :: thesis: for r being Real
for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
let r be Real; :: thesis: for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: Omega --> r is Real-Valued-Random-Variable of Sigma
set E0 = Omega --> 1;
set E = Omega --> r;
reconsider S = Omega as Element of Sigma by MEASURE1:21;
A100: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:19;
reconsider E0 = Omega --> 1 as Function of Omega,REAL by FUNCT_2:9;
K21: R_EAL E0 = chi (S,Omega) by CHILM0;
chi (S,Omega) is_measurable_on S by MESFUNC2:32;
then E0 is_measurable_on S by MESFUNC6:def 6, K21;
then K22: E0 is Real-Valued-Random-Variable of Sigma by RANDOM_1:def 2;
K221: dom (Omega --> r) = dom E0 by A100, FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom (Omega --> r) implies (Omega --> r) . x = r * (E0 . x) )
assume AS1: x in dom (Omega --> r) ; :: thesis: (Omega --> r) . x = r * (E0 . x)
hence (Omega --> r) . x = r * 1 by FUNCOP_1:13
.= r * (E0 . x) by AS1, FUNCOP_1:13 ;
:: thesis: verum

end;

then Omega --> r = r (#) E0 by K221, VALUED_1:def 5;
hence Omega --> r is Real-Valued-Random-Variable of Sigma by K22, RANDOM_1:20; :: thesis: verum