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:7;
A1: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:13;
reconsider E0 = Omega --> 1 as Function of Omega,REAL by FUNCT_2:7;
A2: R_EAL E0 = chi (S,Omega) by Th3;
chi (S,Omega) is_measurable_on S by MESFUNC2:29;
then E0 is_measurable_on S by A2, MESFUNC6:def 1;
then A3: E0 is Real-Valued-Random-Variable of Sigma by RANDOM_1:def 2;
A4: dom (Omega --> r) = dom E0 by A1, FUNCT_2:def 1;

now

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

end;

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