let f be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL implies for E being Element of L-Field holds f is E -measurable )
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL ; :: thesis: for E being Element of L-Field holds f is E -measurable
reconsider A = [.0,+infty.[, B = ].-infty,0.] as Element of L-Field by MEASUR10:5, MEASUR12:75;
A3: A \/ B = REAL by XXREAL_1:172, XXREAL_1:224;
( f is_-infty_improper_integrable_on 0 & f is_+infty_improper_integrable_on 0 ) by A1, A2, INTEGR25:36;
then ( R_EAL f is A -measurable & R_EAL f is B -measurable ) by A1, Th36, Th37, MESFUNC6:def 1;
then R_EAL f is A \/ B -measurable by MESFUNC1:31;
hence for E being Element of L-Field holds f is E -measurable by A3, MESFUNC6:def 1, MESFUNC6:16; :: thesis: verum