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, NUMBERS:19;
A2: R_EAL E0 = chi (S,Omega) by Th3;
chi (S,Omega) is S -measurable by MESFUNC2:29;
then E0 is [#] Sigma -measurable by A2, MESFUNC6:def 1;
then A3: E0 is Real-Valued-Random-Variable of Sigma ;
A4: dom (Omega --> r) = dom E0 by A1, FUNCT_2:def 1;

now :: thesis: for x being object st x in dom (Omega --> r) holds
(Omega --> r) . x = r * (E0 . x)

let x be object ; :: 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