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

suppose A6: f is_+infty_ext_Riemann_integrable_on a ; :: thesis:

then A7: improper_integral_+infty (f,a) = infty_ext_right_integral (f,a) by A3, INTEGR25:27;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = right_closed_halfline a and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A10: Intf is convergent_in+infty and
A11: infty_ext_right_integral (f,a) = lim_in+infty Intf by A6, INTEGR10:def 7;
A12: for p, q being Real st p in dom Intf & q in dom Intf & p < q holds
Intf . p <= Intf . q

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: ( a <= q & q < +infty ) by A8, A14, A5, A2, XXREAL_1:3;
then [.a,q.] c= [.a,+infty.[ by XXREAL_1:43;
then A17: [.a,q.] c= dom f by A1, A5, A2;
A18: [.a,q.] = ['a,q'] by A16, INTEGRA5:def 3;
A19: a <= p by A8, A13, A5, A2, XXREAL_1:3;
A20: ( f is_integrable_on ['a,q'] & f | ['a,q'] is bounded ) by A6, A16, INTEGR10:def 5;
A21: [.a,p.] c= [.a,q.] by A15, XXREAL_1:34;
( Intf . p = integral (f,a,p) & Intf . q = integral (f,a,q) ) by A13, A14, A9;
hence Intf . p <= Intf . q by A17, A20, A4, A21, A19, A18, Th14, MESFUNC6:55; :: thesis:

end;

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

proof

let x be Real; :: thesis:
assume A37: x in dom Intf ; :: thesis:
then A38: ( a <= x & x < +infty ) by A8, A2, A5, XXREAL_1:3;
then A39: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, INTEGR25:def 2;
reconsider AX = [.a,x.] as non empty closed_interval Subset of REAL by A38, XXREAL_1:30, MEASURE5:def 3;
A40: AX = ['a,x'] by A38, INTEGRA5:def 3;
AX c= [.a,+infty.[ by A38, XXREAL_1:43;
then A41: 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 | [.a,x.])) by A41, A39, A40, MESFUN14:49;
then integral (f,AX) = Integral (L-Meas,(f | [.a,x.])) by INTEGRA5:def 2;
then integral (f,a,x) = Integral (L-Meas,(f | [.a,x.])) by A38, A40, INTEGRA5:def 4;
hence Intf . x = Integral (L-Meas,(f | [.a,x.])) by A9, A37; :: thesis:

end;

A42: Partial_Union E = E by A23, PROB_4:15;
A43: for m being Nat holds I . m = integral (f,a,(a + m))

proof

let m be Nat; :: thesis:
A44: ( a <= a + m & a + m < +infty ) by XREAL_0:def 1, XXREAL_0:9, XREAL_1:31;
then A45: f || ['a,(a + m)'] is bounded by A6, INTEGR10:def 5;
A46: ['a,(a + m)'] = [.a,(a + m).] by XREAL_1:31, INTEGRA5:def 3;
then ['a,(a + m)'] c= [.a,+infty.[ by A44, XXREAL_1:43;
then A47: ['a,(a + m)'] c= dom f by A1, A2, A5;
A48: E . m = [.a,(a + m).] by A23;
(R_EAL (f | A)) | (E . m) = (f | A) | (E . m) by MESFUNC5:def 7;
then (R_EAL (f | A)) | (E . m) = f | (E . m) by A48, A44, A5, XXREAL_1:43, RELAT_1:74;
then (R_EAL (f | A)) | (E . m) = R_EAL (f | (E . m)) by MESFUNC5:def 7;
then I . m = Integral (L-Meas,(R_EAL (f | (E . m)))) by A34, A42;
then I . m = Integral (L-Meas,(f | [.a,(a + m).])) by A48, MESFUNC6:def 3;
hence I . m = integral (f,a,(a + m)) by A46, A47, A45, A44, A6, INTEGR10:def 5, 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_right_integral (f,a))).| < p

proof

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

proof

end;

then consider RI being Real such that
A67: ( 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;
A68: RI = Integral (L-Meas,(f | A)) by A35, A67, MESFUNC6:def 3;
for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st R < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1

proof

let g1 be Real; :: thesis:
assume A69: 0 < g1 ; :: thesis:
set g2 = g1 / 2;
consider N being Nat such that
A70: for m being Nat st N <= m holds
|.((I . m) - (lim I)).| < g1 by A69, A67;
take R = a + N; :: thesis:
A71: ( a <= R & R < +infty ) by XREAL_0:def 1, XXREAL_0:9, XREAL_1:31;
then A72: R in dom Intf by A8, A5, A2, XXREAL_1:3;
thus for r1 being Real st R < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 :: thesis:

proof

let r1 be Real; :: thesis:
assume that
A73: R < r1 and
A74: r1 in dom Intf ; :: thesis:
I . N = integral (f,a,(a + N)) by A43;
then Intf . R = I . N by A71, A9, A8, A5, A2, XXREAL_1:3;
then A75: I . N <= Intf . r1 by A73, A72, A74, A12;
( RI - (I . N) = RI - (I . N) & RI - (Intf . r1) = RI - (Intf . r1) ) ;
then A76: RI - (Intf . r1) <= RI - (I . N) by A75, XXREAL_3:37;
A77: |.((I . N) - RI).| < g1 by A70, A67;
reconsider A2 = [.a,r1.] as Element of L-Field by MEASUR10:5, MEASUR12:75;
r1 in REAL by XREAL_0:def 1;
then A78: A2 c= A1 by A5, XXREAL_0:9, XXREAL_1:43;
then Integral (L-Meas,((f | A) | A2)) <= Integral (L-Meas,((f | A) | A1)) by A24, A31, A4, MESFUNC6:55, MESFUNC6:87;
then Integral (L-Meas,(f | A2)) <= RI by A78, A68, RELAT_1:74;
then A79: Intf . r1 <= RI by A74, A36;
then A80: |.((Intf . r1) - RI).| = - ((Intf . r1) - RI) by ABSVALUE:30, XREAL_1:47
.= RI - (Intf . r1) ;
I . N <= RI by A75, A79, 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 A76, A80, A77, XXREAL_0:2; :: thesis:

end;

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

end;

suppose A81: not f is_+infty_ext_Riemann_integrable_on a ; :: thesis:

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

end;