reconsider X = Omega as Element of Sigma by MEASURE1:21;
chi X,Omega is V55() by MESFUNC2:31;
then ( dom (chi X,Omega) = Omega & rng (chi X,Omega) c= REAL ) by FUNCT_3:def 3, VALUED_0:def 3;
then reconsider f = chi X,Omega as Function of Omega,REAL by FUNCT_2:4;
( R_EAL f = chi X,Omega & chi X,Omega is_measurable_on X ) by MESFUNC2:32;
then f is_measurable_on X by MESFUNC6:def 6;
hence ex b₁ being Function of Omega,REAL ex X being Element of Sigma st
( X = Omega & b₁ is_measurable_on X ) ; :: thesis: verum