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 and
A5: not f is_-infty_ext_Riemann_integrable_on b ; :: thesis:
A6: for a being Real st a <= b holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A3, INTEGR25:def 1;
A7: A = ].-infty,b.] by A2, LIMFUNC1:def 1;
then reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;
A8: R_EAL f is A1 -measurable by A1, A2, A7, A3, Th37, MESFUNC6:def 1;
A9: A1 = dom (f | A1) by A1, A2, RELAT_1:62;
then A1 = (dom f) /\ A1 by RELAT_1:61;
then A1 = (dom (R_EAL f)) /\ A1 by MESFUNC5:def 7;
then (R_EAL f) | A1 is A1 -measurable by A8, MESFUNC5:42;
then A10: R_EAL (f | A1) is A1 -measurable by Th16;
f | A1 is nonnegative by A4, MESFUNC6:55;
then A11: R_EAL (f | A1) is nonnegative by MESFUNC5:def 7;
A1 = dom (R_EAL (f | A1)) by A9, MESFUNC5:def 7;
then A12: integral+ (L-Meas,(max- (R_EAL (f | A1)))) < +infty by A10, A11, MESFUN11:53;
A13: A1 = dom (R_EAL (f | A1)) by A9, MESFUNC5:def 7;
consider E being SetSequence of L-Field such that
A14: ( ( for n being Nat holds E . n = [.(b - n),b.] ) & E is non-descending & E is convergent & Union E = ].-infty,b.] ) by Th26;
A15: lim E = Union E by A14, SETLIM_1:80;
then A1 \ (lim E) = {} by A14, A7, XBOOLE_1:37;
then L-Meas . (A1 \ (lim E)) = 0 by VALUED_0:def 19;
then consider I being ExtREAL_sequence such that
A16: for n being Nat holds I . n = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . n))) and
I is convergent and
A17: Integral (L-Meas,(R_EAL (f | A))) = lim I by A10, A13, A12, A14, A15, A7, Th19;
consider Intf being PartFunc of REAL,REAL such that
A18: dom Intf = left_closed_halfline b and
A19: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A20: ( Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) by A3, INTEGR25:def 1;
A21: for x being Real st x in dom Intf holds
Intf . x >= 0

proof

let x be Real; :: thesis:
assume A22: x in dom Intf ; :: thesis:
then A23: ( -infty < x & x <= b ) by A18, A2, A7, XXREAL_1:2;
then reconsider AX = [.x,b.] as non empty closed_interval Subset of REAL by XXREAL_1:30, MEASURE5:def 3;
AX c= ].-infty,b.] by A23, XXREAL_1:39;
then AX c= dom f by A1, A2, A7;
then dom (f | AX) = AX by RELAT_1:62;
then reconsider f1 = f | AX as Function of AX,REAL by FUNCT_2:def 1, RELSET_1:5;
A24: AX = ['x,b'] by A23, INTEGRA5:def 3;
then A25: f1 | AX is bounded by A23, A3, INTEGR25:def 1;
for r being Real st r in AX holds
f1 . r >= 0

proof

let r be Real; :: thesis:
assume A26: r in AX ; :: thesis:
f . r >= 0 by A4, MESFUNC6:51;
hence f1 . r >= 0 by A26, FUNCT_1:49; :: thesis:

end;

then integral f1 >= 0 by A25, INTEGRA2:32;
then integral (f,AX) >= 0 by INTEGRA5:def 2;
then integral (f,x,b) >= 0 by A23, A24, INTEGRA5:def 4;
hence Intf . x >= 0 by A19, A22; :: thesis:

end;

A27: now :: thesis:

assume A28: Intf is divergent_in-infty_to-infty ; :: thesis:
consider r being Real such that
A29: for r1 being Real st r1 < r & r1 in dom Intf holds
Intf . r1 < 0 by A28, LIMFUNC1:49;
consider r1 being Real such that
A30: ( r1 < r & r1 in dom Intf ) by A28, LIMFUNC1:49;
Intf . r1 < 0 by A29, A30;
hence contradiction by A21, A30; :: thesis:

end;

then A31: improper_integral_-infty (f,b) = +infty by A3, A18, A19, A20, A5, A6, INTEGR10:def 6, INTEGR25:def 3;
for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= I . m

proof

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
consider r being Real such that
A32: for r1 being Real st r1 < r & r1 in dom Intf holds
g < Intf . r1 by A27, A18, A19, A20, A5, A6, INTEGR10:def 6, LIMFUNC1:48;
consider r1 being Real such that
A33: ( r1 < r & r1 in dom Intf ) by A27, A18, A19, A20, A5, A6, INTEGR10:def 6, LIMFUNC1:48;
g < Intf . r1 by A32, A33;
then A34: g < integral (f,r1,b) by A33, A19;
A35: ( -infty < r1 & r1 <= b ) by A33, A18, A2, A7, XXREAL_1:2;
consider n being Nat such that
A36: b - r1 < n by SEQ_4:3;
b < r1 + n by A36, XREAL_1:19;
then A37: b - n < r1 by XREAL_1:19;
take n ; :: thesis:
thus for m being Nat st n <= m holds
g <= I . m :: thesis:

proof

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then b - m <= b - n by XREAL_1:10;
then A38: b - m < r1 by A37, XXREAL_0:2;
A39: -infty < b - m by XREAL_0:def 1, XXREAL_0:12;
A40: b - m <= b by XREAL_1:43;
then A41: ( f is_integrable_on ['(b - m),b'] & f | ['(b - m),b'] is bounded ) by A3, INTEGR25:def 1;
A42: ['(b - m),b'] = [.(b - m),b.] by XREAL_1:43, INTEGRA5:def 3;
then ['(b - m),b'] c= ].-infty,b.] by A39, XXREAL_1:39;
then A43: ['(b - m),b'] c= dom f by A1, A7, A2;
r1 in ['(b - m),b'] by A38, A35, A42, XXREAL_1:1;
then A44: integral (f,(b - m),b) = (integral (f,(b - m),r1)) + (integral (f,r1,b)) by A40, A41, A43, INTEGRA6:17;
[.(b - m),r1.] c= ].-infty,b.] by A35, A39, XXREAL_1:39;
then A45: [.(b - m),r1.] c= dom f by A1, A7, A2;
f | [.(b - m),r1.] is bounded by A41, A42, A35, XXREAL_1:34, RFUNCT_1:74;
then integral (f,(b - m),r1) >= 0 by A38, A45, Th12, A4, MESFUNC6:55;
then A46: integral (f,r1,b) <= integral (f,(b - m),b) by A44, XREAL_1:31;
A47: E . m = [.(b - m),b.] by A14;
(R_EAL (f | A)) | (E . m) = (f | A) | (E . m) by MESFUNC5:def 7;
then A48: (R_EAL (f | A)) | (E . m) = f | (E . m) by A47, A39, A7, XXREAL_1:39, RELAT_1:74;
A49: f || ['(b - m),b'] is bounded by A40, A3, INTEGR25:def 1;
I . m = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . m))) by A16
.= Integral (L-Meas,((R_EAL (f | A)) | (E . m))) by A14, PROB_4:15
.= Integral (L-Meas,(R_EAL (f | (E . m)))) by A48, MESFUNC5:def 7
.= Integral (L-Meas,(f | (E . m))) by MESFUNC6:def 3
.= Integral (L-Meas,(f | [.(b - m),b.])) by A14
.= integral (f,(b - m),b) by A49, A40, A42, A43, A3, INTEGR25:def 1, MESFUN14:50 ;
hence g <= I . m by A46, A34, XXREAL_0:2; :: thesis:

end;

then I is convergent_to_+infty by MESFUNC5:def 9;
then A50: lim I = +infty by MESFUNC5:def 12;
hence improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) by A17, A31, MESFUNC6:def 3; :: thesis:
thus Integral (L-Meas,(f | A)) = +infty by A17, A50, MESFUNC6:def 3; :: thesis: