let a be Real; :: thesis: for f being PartFunc of REAL,REAL st [.a,+infty.[ c= dom f & f is_+infty_improper_integrable_on a holds
for E being Element of L-Field st E c= [.a,+infty.[ holds
f is E -measurable
let f be PartFunc of REAL,REAL; :: thesis: ( [.a,+infty.[ c= dom f & f is_+infty_improper_integrable_on a implies for E being Element of L-Field st E c= [.a,+infty.[ holds
f is E -measurable )
assume that
A1: [.a,+infty.[ c= dom f and
A2: f is_+infty_improper_integrable_on a ; :: thesis: for E being Element of L-Field st E c= [.a,+infty.[ holds
f is E -measurable
set A = [.a,+infty.[;
reconsider A = [.a,+infty.[ 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,(a + n).] ) & K is non-descending & K is convergent & Union K = [.a,+infty.[ ) by Th25;
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
A4: a <= a + n by XREAL_1:31;
A5: K . n = [.a,(a + n).] by A3;
then reconsider Kn = K . n as non empty closed_interval Subset of REAL by XREAL_1:31, XXREAL_1:30, MEASURE5:def 3;
Kn = ['a,(a + n)'] by A5, XREAL_1:31, INTEGRA5:def 3;
then A6: ( f is_integrable_on Kn & f || Kn is bounded ) by A4, A2, INTEGR25:def 2;
Kn c= A by A5, XXREAL_1:251;
then Kn c= dom f by A1;
hence R_EAL f is K1 . n -measurable by A6, MESFUN14:49, MESFUNC6:def 1; :: thesis: verum

end;

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