reconsider X = Omega as Element of Sigma by MEASURE1:7;
chi (X,Omega) is V56() by MESFUNC2:28;
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:2;
( R_EAL f = chi (X,Omega) & chi (X,Omega) is_measurable_on X ) by MESFUNC2:29;
then f is_measurable_on X by MESFUNC6:def 1;
hence ex b₁ being Function of Omega,REAL ex X being Element of Sigma st
( X = Omega & b₁ is_measurable_on X ) ; :: thesis: verum