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_right_improper_integrable_on a,b and
A4: f | A is nonnegative and
A5: not f is_right_ext_Riemann_integrable_on a,b ; :: thesis:
A6: for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, INTEGR24:def 2;
reconsider A1 = A as Element of L-Field by A2, MEASUR10:5, MEASUR12:75;
A7: a < b by A2, XXREAL_1:27;
A8: R_EAL f is A1 -measurable by A1, A2, A3, Th33, 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 - ((b - a) / (n + 1))).] & 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, XXREAL_1:27, Th23;
A15: 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, A2, 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,a,x) and
A20: ( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) by A3, INTEGR24:def 2;
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:3;
then reconsider AX = [.a,x.] as non empty closed_interval Subset of REAL by XXREAL_1:30, MEASURE5:def 3;
A24: AX c= [.a,b.[ by A23, XXREAL_1:43;
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 = ['a,x'] by A23, INTEGRA5:def 3;
then A26: f1 | AX is bounded by A23, A3, INTEGR24:def 2;
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,a,x) >= 0 by A23, A25, INTEGRA5:def 4;
hence Intf . x >= 0 by A19, A22; :: thesis:

end;

A28: now :: thesis:

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

end;

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

end;

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