let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonnegative holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
let a, b be Real; :: thesis: for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonnegative holds
( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
let A be non empty Subset of REAL; :: thesis: ( [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & f | A is nonnegative implies ( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) ) )
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 ; :: thesis: ( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
reconsider A1 = A as Element of L-Field by A2, MEASUR10:5, MEASUR12:75;
A5: a < b by A2, XXREAL_1:27;

per cases ( f is_right_ext_Riemann_integrable_on a,b or not f is_right_ext_Riemann_integrable_on a,b ) ;

suppose A6: f is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )

then A7: right_improper_integral (f,a,b) = ext_right_integral (f,a,b) by A3, INTEGR24:39;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = [.a,b.[ and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A10: Intf is_left_convergent_in b and
A11: ext_right_integral (f,a,b) = lim_left (Intf,b) by A6, INTEGR10:def 3;
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: ( p in dom Intf & q in dom Intf & p < q implies Intf . p <= Intf . q )
assume that
A13: p in dom Intf and
A14: q in dom Intf and
A15: p < q ; :: thesis: Intf . p <= Intf . q
A16: ( a <= q & q < b ) by A8, A14, XXREAL_1:3;
then [.a,q.] c= [.a,b.[ by XXREAL_1:43;
then A17: [.a,q.] c= dom f by A1;
A18: [.a,q.] = ['a,q'] by A16, INTEGRA5:def 3;
A19: a <= p by A8, A13, XXREAL_1:3;
A20: ( f is_integrable_on ['a,q'] & f | ['a,q'] is bounded ) by A6, A16, INTEGR10:def 1;
(f | A) | [.a,q.] is nonnegative by A4, MESFUNC6:55;
then A21: f | [.a,q.] is nonnegative by A16, A2, XXREAL_1:43, RELAT_1:74;
A22: [.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, A21, A22, A19, A18, Th14; :: thesis: verum

end;

then A23: Intf is non-decreasing by RFUNCT_2:def 3;
consider E being SetSequence of L-Field such that
A24: ( ( 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, Th23, XXREAL_1:27;
A25: A1 = dom (f | A1) by A1, A2, RELAT_1:62;
then A26: A1 = dom (R_EAL (f | A)) by MESFUNC5:def 7;
A27: lim E = Union E by A24, SETLIM_1:80;
A28: lim E c= A1 by A24, A2, SETLIM_1:80;
A1 \ (lim E) = {} by A24, A2, A27, XBOOLE_1:37;
then A29: L-Meas . (A1 \ (lim E)) = 0 by VALUED_0:def 19;
A30: R_EAL f is A1 -measurable by A1, A2, A3, Th33, MESFUNC6:def 1;
A1 = (dom f) /\ A1 by A25, RELAT_1:61;
then A1 = (dom (R_EAL f)) /\ A1 by MESFUNC5:def 7;
then (R_EAL f) | A is A1 -measurable by A30, MESFUNC5:42;
then A31: R_EAL (f | A) is A1 -measurable by Th16;
A32: R_EAL (f | A) is nonnegative by A4, MESFUNC5:def 7;
then A33: integral+ (L-Meas,(max- (R_EAL (f | A)))) < +infty by A31, A26, MESFUN11:53;
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 A24, A31, A26, A28, A29, A33, 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: ( x in dom Intf implies Intf . x = Integral (L-Meas,(f | [.a,x.])) )
assume A37: x in dom Intf ; :: thesis: Intf . x = Integral (L-Meas,(f | [.a,x.]))
then A38: ( a <= x & x < b ) by A8, XXREAL_1:3;
then A39: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, INTEGR24: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,b.[ by A38, XXREAL_1:43;
then A41: AX c= dom f by A1;
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 A39, A40, A41, 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: verum

end;

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

proof

let m be Nat; :: thesis: I . m = integral (f,a,(b - ((b - a) / (m + 1))))
A44: ( a <= b - ((b - a) / (m + 1)) & b - ((b - a) / (m + 1)) < b ) by A5, Th22;
then A45: f || ['a,(b - ((b - a) / (m + 1)))'] is bounded by A6, INTEGR10:def 1;
A46: ['a,(b - ((b - a) / (m + 1)))'] = [.a,(b - ((b - a) / (m + 1))).] by A44, INTEGRA5:def 3;
then ['a,(b - ((b - a) / (m + 1)))'] c= [.a,b.[ by A44, XXREAL_1:43;
then A47: ['a,(b - ((b - a) / (m + 1)))'] c= dom f by A1;
A48: E . m = [.a,(b - ((b - a) / (m + 1))).] by A24;
(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 A2, A24, RELAT_1:74;
then A49: (R_EAL (f | A)) | (E . m) = R_EAL (f | (E . m)) by MESFUNC5:def 7;
I . m = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . m))) by A34;
then A50: I . m = Integral (L-Meas,(f | [.a,(b - ((b - a) / (m + 1))).])) by A49, A42, A48, MESFUNC6:def 3;
f is_integrable_on ['a,(b - ((b - a) / (m + 1)))'] by A44, A6, INTEGR10:def 1;
hence I . m = integral (f,a,(b - ((b - a) / (m + 1)))) by A50, A44, A46, A47, A45, MESFUN14:50; :: thesis: verum

end;

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

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (ext_right_integral (f,a,b))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (ext_right_integral (f,a,b))).| < p
then consider r being Real such that
A51: r < b and
A52: for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (lim_left (Intf,b))).| < p by A10, LIMFUNC2:41;
set rr = max (a,r);
A53: ( a <= max (a,r) & r <= max (a,r) ) by XXREAL_0:25;
max (a,r) < b by A5, A51, XXREAL_0:29;
then A54: 0 < b - (max (a,r)) by XREAL_1:50;
consider n being Nat such that
A55: (b - a) / (b - (max (a,r))) < n by SEQ_4:3;
n <= n + 1 by NAT_1:13;
then (b - a) / (b - (max (a,r))) < 1 * (n + 1) by A55, XXREAL_0:2;
then (b - a) / (n + 1) < 1 * (b - (max (a,r))) by A54, XREAL_1:113;
then (max (a,r)) + ((b - a) / (n + 1)) < b by XREAL_1:20;
then max (a,r) < b - ((b - a) / (n + 1)) by XREAL_1:20;
then A56: r < b - ((b - a) / (n + 1)) by A53, XXREAL_0:2;
A57: 0 < b - a by A2, XXREAL_1:27, XREAL_1:50;
A58: ( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b ) by A5, Th22;
then A59: b - ((b - a) / (n + 1)) in dom Intf by A8, XXREAL_1:3;
set r1 = b - ((b - a) / (n + 1));
A60: |.((Intf . (b - ((b - a) / (n + 1)))) - (lim_left (Intf,b))).| < p by A52, A56, A59, A58;
take n ; :: thesis: for m being Nat st n <= m holds
|.((I . m) - (ext_right_integral (f,a,b))).| < p
thus for m being Nat st n <= m holds
|.((I . m) - (ext_right_integral (f,a,b))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies |.((I . m) - (ext_right_integral (f,a,b))).| < p )
set rm = b - ((b - a) / (m + 1));
assume n <= m ; :: thesis: |.((I . m) - (ext_right_integral (f,a,b))).| < p
then n + 1 <= m + 1 by XREAL_1:6;
then (b - a) / (n + 1) >= (b - a) / (m + 1) by A57, XREAL_1:118;
then A61: b - ((b - a) / (n + 1)) <= b - ((b - a) / (m + 1)) by XREAL_1:10;
A62: a <= b - ((b - a) / (m + 1)) by A5, Th22;
A63: b - ((b - a) / (m + 1)) < b by A57, XREAL_1:44;
then [.a,(b - ((b - a) / (m + 1))).] c= [.a,b.[ by XXREAL_1:43;
then A64: [.a,(b - ((b - a) / (m + 1))).] c= dom f by A1;
f | ['a,(b - ((b - a) / (m + 1)))'] is bounded by A62, A63, A3, INTEGR24:def 2;
then A65: f | [.a,(b - ((b - a) / (m + 1))).] is bounded by A61, A58, XXREAL_0:2, INTEGRA5:def 3;
A66: f is_integrable_on ['a,(b - ((b - a) / (m + 1)))'] by A62, A63, A3, INTEGR24:def 2;
(f | A) | [.a,(b - ((b - a) / (m + 1))).] is nonnegative by A4, MESFUNC6:55;
then A67: f | [.a,(b - ((b - a) / (m + 1))).] is nonnegative by A63, A2, XXREAL_1:43, RELAT_1:74;
[.a,(b - ((b - a) / (n + 1))).] c= [.a,(b - ((b - a) / (m + 1))).] by A61, XXREAL_1:34;
then integral (f,a,(b - ((b - a) / (n + 1)))) <= integral (f,a,(b - ((b - a) / (m + 1)))) by A58, A64, A65, A66, A67, Th14;
then Intf . (b - ((b - a) / (n + 1))) <= integral (f,a,(b - ((b - a) / (m + 1)))) by A9, A58, A8, XXREAL_1:3;
then A68: Intf . (b - ((b - a) / (n + 1))) <= I . m by A43;
A69: b - ((b - a) / (m + 1)) in dom Intf by A8, A62, A63, XXREAL_1:3;
Intf . (b - ((b - a) / (m + 1))) = integral (f,a,(b - ((b - a) / (m + 1)))) by A9, A8, A62, A63, XXREAL_1:3;
then I . m = Intf . (b - ((b - a) / (m + 1))) by A43;
then I . m <= lim_left (Intf,b) by A10, A23, A69, Th6, A57, XREAL_1:44;
then A70: (lim_left (Intf,b)) - (I . m) >= 0 by XXREAL_3:40;
then - ((lim_left (Intf,b)) - (I . m)) <= 0 ;
then (I . m) - (ext_right_integral (f,a,b)) <= 0 by A11, XXREAL_3:26;
then A71: |.((I . m) - (ext_right_integral (f,a,b))).| = - ((I . m) - (ext_right_integral (f,a,b))) by EXTREAL1:18
.= (ext_right_integral (f,a,b)) - (I . m) by XXREAL_3:26 ;
reconsider EX = ext_right_integral (f,a,b) as ExtReal ;
A72: EX - (Intf . (b - ((b - a) / (n + 1)))) = EX + (- (Intf . (b - ((b - a) / (n + 1))))) by XXREAL_3:def 4
.= (ext_right_integral (f,a,b)) + (- (Intf . (b - ((b - a) / (n + 1))))) by XXREAL_3:def 2
.= (ext_right_integral (f,a,b)) - (Intf . (b - ((b - a) / (n + 1)))) ;
A73: EX - (I . m) <= EX - (Intf . (b - ((b - a) / (n + 1)))) by A68, XXREAL_3:37;
then - ((ext_right_integral (f,a,b)) - (Intf . (b - ((b - a) / (n + 1))))) <= 0 by A72, A70, A11;
then |.((Intf . (b - ((b - a) / (n + 1)))) - (ext_right_integral (f,a,b))).| = - ((Intf . (b - ((b - a) / (n + 1)))) - (ext_right_integral (f,a,b))) by ABSVALUE:30
.= (ext_right_integral (f,a,b)) - (Intf . (b - ((b - a) / (n + 1)))) ;
hence |.((I . m) - (ext_right_integral (f,a,b))).| < p by A60, A11, A72, A73, A71, XXREAL_0:2; :: thesis: verum

end;

end;

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

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex R being Real st
( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 ) ) )
assume A76: 0 < g1 ; :: thesis: ex R being Real st
( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 ) )
set g2 = g1 / 2;
consider N being Nat such that
A77: for m being Nat st N <= m holds
|.((I . m) - (lim I)).| < g1 by A76, A74;
take R = b - ((b - a) / (N + 1)); :: thesis: ( R < b & ( for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 ) )
A78: ( a <= R & R < b ) by A5, Th22;
then A79: R in dom Intf by A8, XXREAL_1:3;
thus R < b by A5, Th22; :: thesis: for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1
thus for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( R < r1 & r1 < b & r1 in dom Intf implies |.((Intf . r1) - RI).| < g1 )
assume that
A80: R < r1 and
A81: r1 < b and
A82: r1 in dom Intf ; :: thesis: |.((Intf . r1) - RI).| < g1
I . N = integral (f,a,(b - ((b - a) / (N + 1)))) by A43;
then Intf . R = I . N by A78, A9, A8, XXREAL_1:3;
then A83: I . N <= Intf . r1 by A80, A79, A82, A12;
( RI - (I . N) = RI - (I . N) & RI - (Intf . r1) = RI - (Intf . r1) ) ;
then A84: RI - (Intf . r1) <= RI - (I . N) by A83, XXREAL_3:37;
A85: |.((I . N) - RI).| < g1 by A77, A74;
reconsider A2 = [.a,r1.] as Element of L-Field by MEASUR10:5, MEASUR12:75;
A2 c= A1 by A2, A81, XXREAL_1:43;
then Integral (L-Meas,((f | A) | A2)) <= Integral (L-Meas,((f | A) | A1)) by A4, A25, A31, MESFUNC6:def 1, MESFUNC6:87;
then Integral (L-Meas,(f | A2)) <= RI by A75, A2, A81, XXREAL_1:43, RELAT_1:74;
then A86: Intf . r1 <= RI by A82, A36;
then A87: |.((Intf . r1) - RI).| = - ((Intf . r1) - RI) by ABSVALUE:30, XREAL_1:47;
I . N <= RI by A83, A86, XXREAL_0:2;
then |.(RI - (I . N)).| = RI - (I . N) by XXREAL_3:40, EXTREAL1:def 1;
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 A84, A87, A85, XXREAL_0:2; :: thesis: verum

end;

end;

hence right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A11, A7, A75, A10, LIMFUNC2:41; :: thesis: ( ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
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 A4, A31, A25, MESFUNC6:def 1, MESFUNC6:82;
then integral+ (L-Meas,(max+ (R_EAL (f | A)))) < +infty by A75, XREAL_0:def 1, XXREAL_0:9;
hence ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) by A31, A26, A33, MESFUNC5:def 17, MESFUNC6:def 4; :: thesis: ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty )
thus ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) by A6; :: thesis: verum

end;

suppose A88: not f is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )

hence right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A1, A2, A3, A4, Lm8; :: thesis: ( ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
thus ( f is_right_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) by A88; :: thesis: ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty )
thus ( not f is_right_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) by A1, A2, A3, A4, Lm8; :: thesis: verum

end;

end;