let Omega be non empty set ; :: thesis:
let r be Real; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
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;

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

end;