let f be PartFunc of REAL,REAL; :: thesis:
let b be Real; :: thesis:
let A be non empty Subset of REAL; :: thesis:
assume that
A1: left_closed_halfline b c= dom f and
A2: A = left_closed_halfline b and
A3: f is_-infty_improper_integrable_on b and
A4: f is nonnegative ; :: thesis:
A5: A = ].-infty,b.] by A2, LIMFUNC1:def 1;
then reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;

suppose A6: f is_-infty_ext_Riemann_integrable_on b ; :: thesis:

then A7: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A3, INTEGR25:22;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = left_closed_halfline b and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A10: Intf is convergent_in-infty and
A11: infty_ext_left_integral (f,b) = lim_in-infty Intf by A6, INTEGR10:def 8;
A12: for p, q being Real st p in dom Intf & q in dom Intf & p < q holds
Intf . q <= Intf . p

proof

let p, q be Real; :: thesis:
assume that
A13: p in dom Intf and
A14: q in dom Intf and
A15: p < q ; :: thesis:
A16: ( -infty < p & p <= b ) by A8, A13, A5, A2, XXREAL_1:2;
then [.p,b.] c= ].-infty,b.] by XXREAL_1:39;
then A17: [.p,b.] c= dom f by A1, A5, A2;
A18: [.p,b.] = ['p,b'] by A16, INTEGRA5:def 3;
A19: q <= b by A8, A14, A5, A2, XXREAL_1:2;
A20: ( f is_integrable_on ['p,b'] & f | ['p,b'] is bounded ) by A6, A16, INTEGR10:def 6;
A21: [.q,b.] c= [.p,b.] by A15, XXREAL_1:34;
( Intf . p = integral (f,p,b) & Intf . q = integral (f,q,b) ) by A13, A14, A9;
hence Intf . q <= Intf . p by A17, A20, A21, A19, A18, Th14, A4, MESFUNC6:55; :: thesis:

end;

then A22: Intf is non-increasing by RFUNCT_2:def 4;
consider E being SetSequence of L-Field such that
A23: ( ( for n being Nat holds E . n = [.(b - n),b.] ) & E is non-descending & E is convergent & Union E = ].-infty,b.] ) by Th26;
A24: A1 = dom (f | A1) by A1, A2, RELAT_1:62;
then A25: A1 = dom (R_EAL (f | A)) by MESFUNC5:def 7;
A26: lim E c= A1 by A23, A5, SETLIM_1:80;
lim E = Union E by A23, SETLIM_1:80;
then A1 \ (lim E) = {} by A23, A5, XBOOLE_1:37;
then A27: L-Meas . (A1 \ (lim E)) = 0 by VALUED_0:def 19;
A28: R_EAL f is A1 -measurable by A1, A2, A3, A5, Th37, MESFUNC6:def 1;
A1 = (dom f) /\ A1 by A24, RELAT_1:61;
then A1 = (dom (R_EAL f)) /\ A1 by MESFUNC5:def 7;
then (R_EAL f) | A is A1 -measurable by A28, MESFUNC5:42;
then A29: R_EAL (f | A) is A1 -measurable by Th16;
then A30: f | A is A1 -measurable by MESFUNC6:def 1;
f | A is nonnegative by A4, MESFUNC6:55;
then A31: R_EAL (f | A) is nonnegative by MESFUNC5:def 7;
then A32: integral+ (L-Meas,(max- (R_EAL (f | A)))) < +infty by A29, A25, MESFUN11:53;
consider I being ExtREAL_sequence such that
A33: for n being Nat holds I . n = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . n))) and
I is convergent and
A34: Integral (L-Meas,(R_EAL (f | A))) = lim I by A23, A29, A25, A26, A27, A32, Th19;
A35: for x being Real st x in dom Intf holds
Intf . x = Integral (L-Meas,(f | [.x,b.]))

proof

let x be Real; :: thesis:
assume A36: x in dom Intf ; :: thesis:
then A37: ( -infty < x & x <= b ) by A8, A2, A5, XXREAL_1:2;
then A38: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, INTEGR25:def 1;
reconsider AX = [.x,b.] as non empty closed_interval Subset of REAL by A37, XXREAL_1:30, MEASURE5:def 3;
A39: AX = ['x,b'] by A37, INTEGRA5:def 3;
AX c= ].-infty,b.] by A37, XXREAL_1:39;
then A40: AX c= dom f by A1, A2, A5;
reconsider AX1 = AX as Element of L-Field by MEASUR10:5, MEASUR12:75;
AX = AX1 ;
then integral (f || AX) = Integral (L-Meas,(f | [.x,b.])) by A38, A39, A40, MESFUN14:49;
then integral (f,AX) = Integral (L-Meas,(f | [.x,b.])) by INTEGRA5:def 2;
then integral (f,x,b) = Integral (L-Meas,(f | [.x,b.])) by A37, A39, INTEGRA5:def 4;
hence Intf . x = Integral (L-Meas,(f | [.x,b.])) by A9, A36; :: thesis:

end;

A41: for m being Nat holds I . m = integral (f,(b - m),b)

proof

let m be Nat; :: thesis:
A42: ( -infty < b - m & b - m <= b ) by XREAL_0:def 1, XXREAL_0:12, XREAL_1:43;
then A43: f || ['(b - m),b'] is bounded by A6, INTEGR10:def 6;
A44: ['(b - m),b'] = [.(b - m),b.] by XREAL_1:43, INTEGRA5:def 3;
then ['(b - m),b'] c= ].-infty,b.] by A42, XXREAL_1:39;
then A45: ['(b - m),b'] c= dom f by A1, A2, A5;
A46: E . m = [.(b - m),b.] by A23;
(R_EAL (f | A)) | (E . m) = (f | A) | (E . m) by MESFUNC5:def 7;
then A47: (R_EAL (f | A)) | (E . m) = f | (E . m) by A46, A42, A5, XXREAL_1:39, RELAT_1:74;
Partial_Union E = E by A23, PROB_4:15;
then I . m = Integral (L-Meas,((R_EAL (f | A)) | (E . m))) by A33;
then I . m = Integral (L-Meas,(R_EAL (f | (E . m)))) by A47, MESFUNC5:def 7;
then I . m = Integral (L-Meas,(f | (E . m))) by MESFUNC6:def 3;
hence I . m = integral (f,(b - m),b) by A6, A42, A46, A44, A45, A43, INTEGR10:def 6, MESFUN14:50; :: thesis:

end;

for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (infty_ext_left_integral (f,b))).| < p

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider r being Real such that
A48: for r1 being Real st r1 < r & r1 in dom Intf holds
|.((Intf . r1) - (lim_in-infty Intf)).| < p by A10, LIMFUNC1:78;
set rr = min (b,r);
consider n being Nat such that
A49: b - r < n by SEQ_4:3;
set r1 = b - n;
A50: b < r + n by A49, XREAL_1:19;
A51: ( -infty < b - n & b - n <= b ) by XREAL_0:def 1, XXREAL_0:12, XREAL_1:43;
then b - n in dom Intf by A2, A5, A8, XXREAL_1:2;
then A52: |.((Intf . (b - n)) - (lim_in-infty Intf)).| < p by A48, A50, XREAL_1:19;
take n ; :: thesis:
thus for m being Nat st n <= m holds
|.((I . m) - (infty_ext_left_integral (f,b))).| < p :: thesis:

proof

end;

then consider RI being Real such that
A63: ( lim I = RI & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (lim I)).| < p ) ) by MESFUNC5:def 8, MESFUNC9:7;
A64: RI = Integral (L-Meas,(f | A)) by A34, A63, MESFUNC6:def 3;
for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st r1 < R & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1

proof

let g1 be Real; :: thesis:
assume A65: 0 < g1 ; :: thesis:
set g2 = g1 / 2;
consider N being Nat such that
A66: for m being Nat st N <= m holds
|.((I . m) - (lim I)).| < g1 by A65, A63;
take R = b - N; :: thesis:
A67: ( -infty < R & R <= b ) by XREAL_0:def 1, XXREAL_0:12, XREAL_1:43;
then A68: R in dom Intf by A8, A5, A2, XXREAL_1:2;
thus for r1 being Real st r1 < R & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 :: thesis:

proof

let r1 be Real; :: thesis:
assume that
A69: r1 < R and
A70: r1 in dom Intf ; :: thesis:
I . N = integral (f,(b - N),b) by A41;
then A71: Intf . R = I . N by A67, A9, A8, A5, A2, XXREAL_1:2;
A72: I . N <= Intf . r1 by A71, A69, A68, A70, A12;
( RI - (I . N) = RI - (I . N) & RI - (Intf . r1) = RI - (Intf . r1) ) ;
then A73: RI - (Intf . r1) <= RI - (I . N) by A72, XXREAL_3:37;
A74: |.((I . N) - RI).| < g1 by A66, A63;
reconsider A2 = [.r1,b.] as Element of L-Field by MEASUR10:5, MEASUR12:75;
r1 in REAL by XREAL_0:def 1;
then A75: A2 c= A1 by A5, XXREAL_0:12, XXREAL_1:39;
then Integral (L-Meas,((f | A) | A2)) <= Integral (L-Meas,((f | A) | A1)) by A24, A30, A4, MESFUNC6:55, MESFUNC6:87;
then Integral (L-Meas,(f | A2)) <= RI by A64, A75, RELAT_1:74;
then A76: Intf . r1 <= RI by A70, A35;
then A77: |.((Intf . r1) - RI).| = - ((Intf . r1) - RI) by ABSVALUE:30, XREAL_1:47
.= RI - (Intf . r1) ;
I . N <= RI by A72, A76, XXREAL_0:2;
then |.(RI - (I . N)).| = RI - (I . N) by EXTREAL1:def 1, XXREAL_3:40;
then |.(- (RI - (I . N))).| = RI - (I . N) by EXTREAL1:29;
then |.((I . N) - RI).| = RI - (I . N) by XXREAL_3:26;
hence |.((Intf . r1) - RI).| < g1 by A73, A77, A74, XXREAL_0:2; :: thesis:

end;

hence improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) by A10, A11, A7, A64, LIMFUNC1:78; :: thesis:
max+ (R_EAL (f | A)) = R_EAL (f | A) by A31, MESFUN11:31;
then Integral (L-Meas,(f | A)) = integral+ (L-Meas,(max+ (R_EAL (f | A)))) by A30, A24, A4, MESFUNC6:55, MESFUNC6:82;
then integral+ (L-Meas,(max+ (R_EAL (f | A)))) < +infty by A64, XREAL_0:def 1, XXREAL_0:9;
hence ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) by A29, A25, A32, MESFUNC5:def 17, MESFUNC6:def 4; :: thesis:
thus ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = +infty ) by A6; :: thesis:

end;

suppose A78: not f is_-infty_ext_Riemann_integrable_on b ; :: thesis:

hence improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) by A1, A2, A3, A4, Lm9; :: thesis:
thus ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) by A78; :: thesis:
thus ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = +infty ) by A1, A2, A3, A4, Lm9; :: thesis:

end;