let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable
let f be PartFunc of REAL,REAL; :: thesis: ( ].a,b.] c= dom f & f is_left_improper_integrable_on a,b implies for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable )
assume that
A1: ].a,b.] c= dom f and
A2: f is_left_improper_integrable_on a,b ; :: thesis: for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable

per cases ( a < b or a >= b ) ;

suppose A3: a < b ; :: thesis: for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable

then reconsider A = ].a,b.] as non empty Subset of REAL by XXREAL_1:32;
reconsider A = A as Element of L-Field by MEASUR12:72, MEASUR12:75;
set dif = b - a;
consider K being SetSequence of L-Field such that
A4: ( ( for n being Nat holds
( K . n = [.(a + ((b - a) / (n + 1))),b.] & K . n c= ].a,b.] & K . n is non empty closed_interval Subset of REAL ) ) & K is non-descending & K is convergent & Union K = ].a,b.] ) by A3, Th24;
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 < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b ) by A3, Th22;
reconsider Kn = K . n as non empty closed_interval Subset of REAL by A4;
Kn = [.(a + ((b - a) / (n + 1))),b.] by A4;
then Kn = ['(a + ((b - a) / (n + 1))),b'] by A5, INTEGRA5:def 3;
then A6: ( f is_integrable_on Kn & f || Kn is bounded ) by A5, A2, INTEGR24:def 1;
Kn c= A by A4;
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 f is Union K1 -measurable by Th21, MESFUNC6:def 1;
hence for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable by A4, MESFUNC6:16; :: thesis: verum

end;

suppose a >= b ; :: thesis: for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable

then A7: ].a,b.] = {} by XXREAL_1:26;

hereby :: thesis: verum

let E be Element of L-Field ; :: thesis: ( E c= ].a,b.] implies f is E -measurable )
assume E c= ].a,b.] ; :: thesis: f is E -measurable
then E = {} by A7;
hence f is E -measurable by Th30; :: thesis: verum

end;

end;

end;