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