reconsider f = chi (E,X) as PartFunc of X,ExtREAL ;
take f ; :: thesis: f is E -measurable
thus f is E -measurable by MESFUNC2:29; :: thesis: verum