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

take f ; :: thesis: f is E -measurable

thus f is E -measurable by MESFUNC2:29; :: thesis: verum