reconsider X = [#] Sigma as Element of Sigma ;
chi (X,Omega) is V70() 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 X -measurable ) by MESFUNC2:29;
then f is X -measurable ;
hence ex b₁ being Function of Omega,REAL st b₁ is [#] Sigma -measurable ; :: thesis: verum