let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
let A be non empty Subset of REAL; :: thesis:
assume that
A1: ].a,b.] c= dom f and
A2: A = ].a,b.] and
A3: f is_left_improper_integrable_on a,b and
A4: f | A is nonnegative and
A5: not f is_left_ext_Riemann_integrable_on a,b ; :: thesis:
A6: for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, INTEGR24:def 1;
reconsider A1 = A as Element of L-Field by A2, MEASUR10:5, MEASUR12:75;
A7: a < b by A2, XXREAL_1:26;
A8: R_EAL f is A1 -measurable by A1, A2, A3, Th34, 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;
A11: R_EAL (f | A1) is nonnegative by A4, 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 = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = ].a,b.] ) by A2, Th24, XXREAL_1:26;
A15: lim E c= A1 by A14, A2, SETLIM_1:80;
lim E = Union E by A14, SETLIM_1:80;
then A1 \ (lim E) = {} by A14, A2, 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, Th19;
consider Intf being PartFunc of REAL,REAL such that
A18: dom Intf = ].a,b.] and
A19: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A20: ( Intf is_right_convergent_in a or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) by A3, INTEGR24: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: ( a < x & x <= b ) by A18, XXREAL_1:2;
then reconsider AX = [.x,b.] as non empty closed_interval Subset of REAL by XXREAL_1:30, MEASURE5:def 3;
A24: AX c= ].a,b.] by A23, XXREAL_1:39;
then AX c= dom f by A1;
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;
A25: AX = ['x,b'] by A23, INTEGRA5:def 3;
then A26: f1 | AX is bounded by A23, A3, INTEGR24:def 1;
for r being Real st r in AX holds
f1 . r >= 0

proof

let r be Real; :: thesis:
assume A27: r in AX ; :: thesis:
(f | A) . r >= 0 by A4, MESFUNC6:51;
then f . r >= 0 by A27, A24, A2, FUNCT_1:49;
hence f1 . r >= 0 by A27, FUNCT_1:49; :: thesis:

end;

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

end;

A28: now :: thesis:

assume A29: Intf is_right_divergent_to-infty_in a ; :: thesis:
then consider r being Real such that
A30: a < r and
A31: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
Intf . r1 < 0 by LIMFUNC2:12;
consider r1 being Real such that
A32: ( r1 < r & a < r1 & r1 in dom Intf ) by A29, A30, LIMFUNC2:12;
Intf . r1 < 0 by A31, A32;
hence contradiction by A21, A32; :: thesis:

end;

then A33: left_improper_integral (f,a,b) = +infty by A3, A18, A19, A5, A6, A20, INTEGR10:def 2, INTEGR24: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
A34: a < r and
A35: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
g < Intf . r1 by A28, A18, A19, A5, A6, A20, INTEGR10:def 2, LIMFUNC2:11;
consider r1 being Real such that
A36: ( r1 < r & a < r1 & r1 in dom Intf ) by A28, A34, A18, A19, A5, A6, A20, INTEGR10:def 2, LIMFUNC2:11;
g < Intf . r1 by A35, A36;
then A37: g < integral (f,r1,b) by A36, A19;
A38: ( a < r1 & r1 <= b ) by A36, A18, XXREAL_1:2;
A39: ( 0 < r1 - a & 0 < b - a ) by A36, A2, XXREAL_1:26, XREAL_1:50;
consider n being Nat such that
A40: (b - a) / (r1 - a) < n by SEQ_4:3;
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 n <= m + 1 by NAT_1:13;
then A41: (b - a) / (r1 - a) < 1 * (m + 1) by A40, XXREAL_0:2;
(b - a) / (m + 1) < 1 * (r1 - a) by A39, A41, XREAL_1:113;
then A42: a + ((b - a) / (m + 1)) < r1 by XREAL_1:20;
A43: a + ((b - a) / (m + 1)) <= b by A7, Th22;
A44: a < a + ((b - a) / (m + 1)) by A7, Th22;
then A45: ( f is_integrable_on ['(a + ((b - a) / (m + 1))),b'] & f | ['(a + ((b - a) / (m + 1))),b'] is bounded ) by A43, A3, INTEGR24:def 1;
A46: ['(a + ((b - a) / (m + 1))),b'] = [.(a + ((b - a) / (m + 1))),b.] by A43, INTEGRA5:def 3;
then ['(a + ((b - a) / (m + 1))),b'] c= ].a,b.] by A44, XXREAL_1:39;
then A47: ['(a + ((b - a) / (m + 1))),b'] c= dom f by A1;
r1 in ['(a + ((b - a) / (m + 1))),b'] by A38, A42, A46, XXREAL_1:1;
then A48: integral (f,(a + ((b - a) / (m + 1))),b) = (integral (f,(a + ((b - a) / (m + 1))),r1)) + (integral (f,r1,b)) by A43, A45, A47, INTEGRA6:17;
[.(a + ((b - a) / (m + 1))),r1.] c= ].a,b.] by A38, A44, XXREAL_1:39;
then A49: [.(a + ((b - a) / (m + 1))),r1.] c= dom f by A1;
A50: f | [.(a + ((b - a) / (m + 1))),r1.] is bounded by A45, A46, A38, XXREAL_1:34, RFUNCT_1:74;
(f | A) | [.(a + ((b - a) / (m + 1))),r1.] is nonnegative by A4, MESFUNC6:55;
then f | [.(a + ((b - a) / (m + 1))),r1.] is nonnegative by A2, A38, A44, XXREAL_1:39, RELAT_1:74;
then integral (f,(a + ((b - a) / (m + 1))),r1) >= 0 by A42, A49, A50, Th12;
then A51: integral (f,r1,b) <= integral (f,(a + ((b - a) / (m + 1))),b) by A48, XREAL_1:31;
(R_EAL (f | A)) | (E . m) = (f | A) | (E . m) by MESFUNC5:def 7;
then A52: (R_EAL (f | A)) | (E . m) = f | (E . m) by A2, A14, RELAT_1:74;
A53: f || ['(a + ((b - a) / (m + 1))),b'] is bounded by A44, A43, A3, INTEGR24: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 A52, MESFUNC5:def 7
.= Integral (L-Meas,(f | (E . m))) by MESFUNC6:def 3
.= Integral (L-Meas,(f | [.(a + ((b - a) / (m + 1))),b.])) by A14
.= integral (f,(a + ((b - a) / (m + 1))),b) by A53, A43, A45, A46, A47, MESFUN14:50 ;
hence g <= I . m by A51, A37, XXREAL_0:2; :: thesis:

end;

then I is convergent_to_+infty by MESFUNC5:def 9;
then A54: Integral (L-Meas,(R_EAL (f | A))) = +infty by A17, MESFUNC5:def 12;
hence left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A33, MESFUNC6:def 3; :: thesis:
thus Integral (L-Meas,(f | A)) = +infty by A54, MESFUNC6:def 3; :: thesis: