let a be Real; :: thesis: for f being PartFunc of REAL,REAL st ].-infty,a.] c= dom f & f is_-infty_improper_integrable_on a holds
for E being Element of L-Field st E c= ].-infty,a.] holds
f is E -measurable
let f be PartFunc of REAL,REAL; :: thesis: ( ].-infty,a.] c= dom f & f is_-infty_improper_integrable_on a implies for E being Element of L-Field st E c= ].-infty,a.] holds
f is E -measurable )
assume that
A1: ].-infty,a.] c= dom f and
A2: f is_-infty_improper_integrable_on a ; :: thesis: for E being Element of L-Field st E c= ].-infty,a.] holds
f is E -measurable
set A = ].-infty,a.];
reconsider A = ].-infty,a.] as Element of L-Field by MEASUR12:72, MEASUR12:75;
consider K being SetSequence of L-Field such that
A3: ( ( for n being Nat holds K . n = [.(a - n),a.] ) & K is non-descending & K is convergent & Union K = ].-infty,a.] ) by Th26;
A4: for n being Element of NAT holds K . n is non empty closed_interval Subset of REAL

proof

let n be Element of NAT ; :: thesis: K . n is non empty closed_interval Subset of REAL
K . n = [.(a - n),a.] by A3;
hence K . n is non empty closed_interval Subset of REAL by XREAL_1:43, XXREAL_1:30, MEASURE5:def 3; :: thesis: verum

end;

rng K c= L-Field ;
then reconsider K1 = K as sequence of L-Field by FUNCT_2:6;
for n being Nat holds R_EAL f is K1 . n -measurable

proof

let n be Nat; :: thesis: R_EAL f is K1 . n -measurable
A5: a - n <= a by XREAL_1:43;
n is Element of NAT by ORDINAL1:def 12;
then reconsider Kn = K . n as non empty closed_interval Subset of REAL by A4;
A6: Kn = [.(a - n),a.] by A3;
then Kn = ['(a - n),a'] by XREAL_1:43, INTEGRA5:def 3;
then A7: ( f is_integrable_on Kn & f || Kn is bounded ) by A5, A2, INTEGR25:def 1;
Kn c= A by A6, XXREAL_1:265;
then Kn c= dom f by A1;
hence R_EAL f is K1 . n -measurable by A7, MESFUN14:49, MESFUNC6:def 1; :: thesis: verum

end;

then R_EAL f is Union K1 -measurable by Th21;
hence for E being Element of L-Field st E c= ].-infty,a.] holds
f is E -measurable by A3, MESFUNC6:def 1, MESFUNC6:16; :: thesis: verum