let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st [.a,b.[ c= dom f & f is_right_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_right_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_right_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

reconsider A = [.a,b.[ 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 - ((b - a) / (n + 1))).] & 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 ) by A3, Th23;
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
not K . n is empty by A4;
then [.a,(b - ((b - a) / (n + 1))).] <> {} by A4;
then A5: a <= b - ((b - a) / (n + 1)) by XXREAL_1:29;
K . n c= [.a,b.[ by A4;
then [.a,(b - ((b - a) / (n + 1))).] c= [.a,b.[ by A4;
then A6: ( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b ) by A5, XXREAL_1:54;
reconsider Kn = K . n as non empty closed_interval Subset of REAL by A4;
Kn = [.a,(b - ((b - a) / (n + 1))).] by A4;
then Kn = ['a,(b - ((b - a) / (n + 1)))'] by XXREAL_1:29, INTEGRA5:def 3;
then A7: ( f is_integrable_on Kn & f || Kn is bounded ) by A6, A2, INTEGR24:def 2;
Kn c= [.a,b.[ by A4;
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 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 A8: [.a,b.[ = {} by XXREAL_1:27;

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 A8;
hence f is E -measurable by Th30; :: thesis: verum

end;

end;

end;