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_left_improper_integrable_on a,b & f | A is nonnegative holds
( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_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_left_improper_integrable_on a,b & f | A is nonnegative holds
( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_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_left_improper_integrable_on a,b & f | A is nonnegative implies ( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_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_left_improper_integrable_on a,b and
A4: f | A is nonnegative ; :: thesis: ( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_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:26;

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

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

then A7: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, INTEGR24:34;
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,x,b) and
A10: Intf is_right_convergent_in a and
A11: ext_left_integral (f,a,b) = lim_right (Intf,a) by A6, INTEGR10:def 4;
A12: for p, q being Real st p in dom Intf & q in dom Intf & p < q holds
Intf . q <= Intf . p

proof

let p, q be Real; :: thesis: ( p in dom Intf & q in dom Intf & p < q implies Intf . q <= Intf . p )
assume that
A13: p in dom Intf and
A14: q in dom Intf and
A15: p < q ; :: thesis: Intf . q <= Intf . p
A16: ( a < p & p <= b ) by A8, A13, XXREAL_1:2;
then [.p,b.] c= ].a,b.] by XXREAL_1:39;
then A17: [.p,b.] c= dom f by A1;
A18: [.p,b.] = ['p,b'] by A16, INTEGRA5:def 3;
A19: q <= b by A8, A14, XXREAL_1:2;
A20: ( f is_integrable_on ['p,b'] & f | ['p,b'] is bounded ) by A6, A16, INTEGR10:def 2;
(f | A) | [.p,b.] is nonnegative by A4, MESFUNC6:55;
then A21: f | [.p,b.] is nonnegative by A2, A16, XXREAL_1:39, RELAT_1:74;
A22: [.q,b.] c= [.p,b.] by A15, XXREAL_1:34;
( Intf . p = integral (f,p,b) & Intf . q = integral (f,q,b) ) by A13, A14, A9;
hence Intf . q <= Intf . p by A17, A20, A21, A22, A19, A18, Th14; :: thesis: verum

end;

then A23: Intf is non-increasing by RFUNCT_2:def 4;
consider E being SetSequence of L-Field such that
A24: ( ( 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;
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, Th34, 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 | [.x,b.]))

proof

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

proof

let m be Nat; :: thesis: I . m = integral (f,(a + ((b - a) / (m + 1))),b)
A44: ( a < a + ((b - a) / (m + 1)) & a + ((b - a) / (m + 1)) <= b ) by A5, Th22;
then A45: f || ['(a + ((b - a) / (m + 1))),b'] is bounded by A6, INTEGR10:def 2;
A46: ['(a + ((b - a) / (m + 1))),b'] = [.(a + ((b - a) / (m + 1))),b.] by A44, 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;
A48: E . m = [.(a + ((b - a) / (m + 1))),b.] 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 A24, A2, 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 - a) / (m + 1))),b.])) by A42, A49, A48, MESFUNC6:def 3;
f is_integrable_on ['(a + ((b - a) / (m + 1))),b'] by A44, A6, INTEGR10:def 2;
hence I . m = integral (f,(a + ((b - a) / (m + 1))),b) 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_left_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_left_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_left_integral (f,a,b))).| < p
then consider r being Real such that
A51: a < r and
A52: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (lim_right (Intf,a))).| < p by A10, LIMFUNC2:42;
set rr = min (b,r);
A53: ( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
a < min (b,r) by A5, A51, XXREAL_0:21;
then A54: 0 < (min (b,r)) - a by XREAL_1:50;
consider n being Nat such that
A55: (b - a) / ((min (b,r)) - a) < n by SEQ_4:3;
n <= n + 1 by NAT_1:13;
then (b - a) / ((min (b,r)) - a) < 1 * (n + 1) by A55, XXREAL_0:2;
then (b - a) / (n + 1) < 1 * ((min (b,r)) - a) by A54, XREAL_1:113;
then a + ((b - a) / (n + 1)) < min (b,r) by XREAL_1:20;
then A56: a + ((b - a) / (n + 1)) < r by A53, XXREAL_0:2;
A57: 0 < b - a by A2, XXREAL_1:26, XREAL_1:50;
A58: ( a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b ) by A5, Th22;
then A59: a + ((b - a) / (n + 1)) in dom Intf by A8, XXREAL_1:2;
set r1 = a + ((b - a) / (n + 1));
A60: |.((Intf . (a + ((b - a) / (n + 1)))) - (lim_right (Intf,a))).| < p by A52, A56, A59, A58;
take n ; :: thesis: for m being Nat st n <= m holds
|.((I . m) - (ext_left_integral (f,a,b))).| < p
thus for m being Nat st n <= m holds
|.((I . m) - (ext_left_integral (f,a,b))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies |.((I . m) - (ext_left_integral (f,a,b))).| < p )
set rm = a + ((b - a) / (m + 1));
assume n <= m ; :: thesis: |.((I . m) - (ext_left_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: a + ((b - a) / (n + 1)) >= a + ((b - a) / (m + 1)) by XREAL_1:6;
A62: a + ((b - a) / (m + 1)) <= b by A5, Th22;
A63: a < a + ((b - a) / (m + 1)) by A57, XREAL_1:29;
then [.(a + ((b - a) / (m + 1))),b.] c= ].a,b.] by XXREAL_1:39;
then A64: [.(a + ((b - a) / (m + 1))),b.] c= dom f by A1;
f | ['(a + ((b - a) / (m + 1))),b'] is bounded by A62, A63, A3, INTEGR24:def 1;
then A65: f | [.(a + ((b - a) / (m + 1))),b.] is bounded by A61, A58, XXREAL_0:2, INTEGRA5:def 3;
A66: f is_integrable_on ['(a + ((b - a) / (m + 1))),b'] by A62, A63, A3, INTEGR24:def 1;
(f | A) | [.(a + ((b - a) / (m + 1))),b.] is nonnegative by A4, MESFUNC6:55;
then A67: f | [.(a + ((b - a) / (m + 1))),b.] is nonnegative by A2, A63, XXREAL_1:39, RELAT_1:74;
[.(a + ((b - a) / (n + 1))),b.] c= [.(a + ((b - a) / (m + 1))),b.] by A61, XXREAL_1:34;
then integral (f,(a + ((b - a) / (n + 1))),b) <= integral (f,(a + ((b - a) / (m + 1))),b) by A58, A64, A65, A66, A67, Th14;
then Intf . (a + ((b - a) / (n + 1))) <= integral (f,(a + ((b - a) / (m + 1))),b) by A9, A58, A8, XXREAL_1:2;
then A68: Intf . (a + ((b - a) / (n + 1))) <= I . m by A43;
A69: a + ((b - a) / (m + 1)) in dom Intf by A8, A62, A63, XXREAL_1:2;
Intf . (a + ((b - a) / (m + 1))) = integral (f,(a + ((b - a) / (m + 1))),b) by A9, A8, A62, A63, XXREAL_1:2;
then I . m = Intf . (a + ((b - a) / (m + 1))) by A43;
then I . m <= lim_right (Intf,a) by A10, A23, A69, Th9, A57, XREAL_1:29;
then A70: (lim_right (Intf,a)) - (I . m) >= 0 by XXREAL_3:40;
then - ((lim_right (Intf,a)) - (I . m)) <= 0 ;
then (I . m) - (ext_left_integral (f,a,b)) <= 0 by A11, XXREAL_3:26;
then A71: |.((I . m) - (ext_left_integral (f,a,b))).| = - ((I . m) - (ext_left_integral (f,a,b))) by EXTREAL1:18
.= (ext_left_integral (f,a,b)) - (I . m) by XXREAL_3:26 ;
reconsider EX = ext_left_integral (f,a,b) as ExtReal ;
A72: EX - (Intf . (a + ((b - a) / (n + 1)))) = EX + (- (Intf . (a + ((b - a) / (n + 1))))) by XXREAL_3:def 4
.= (ext_left_integral (f,a,b)) + (- (Intf . (a + ((b - a) / (n + 1))))) by XXREAL_3:def 2
.= (ext_left_integral (f,a,b)) - (Intf . (a + ((b - a) / (n + 1)))) ;
A73: EX - (I . m) <= EX - (Intf . (a + ((b - a) / (n + 1)))) by A68, XXREAL_3:37;
then - ((ext_left_integral (f,a,b)) - (Intf . (a + ((b - a) / (n + 1))))) <= 0 by A72, A70, A11;
then |.((Intf . (a + ((b - a) / (n + 1)))) - (ext_left_integral (f,a,b))).| = - ((Intf . (a + ((b - a) / (n + 1)))) - (ext_left_integral (f,a,b))) by ABSVALUE:30;
hence |.((I . m) - (ext_left_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
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 ) ) )
assume A76: 0 < g1 ; :: thesis: ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & 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 = a + ((b - a) / (N + 1)); :: thesis: ( a < R & ( for r1 being Real st r1 < R & a < r1 & 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:2;
thus a < R by A5, Th22; :: thesis: for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1
thus for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - RI).| < g1 :: thesis: verum

proof

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

end;

end;

hence left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A11, A7, A75, A10, LIMFUNC2:42; :: thesis: ( ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_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 A31, A25, A4, 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_left_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_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty )
thus ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) by A6; :: thesis: verum

end;

suppose A89: not f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )

hence left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A1, A2, A3, A4, Lm7; :: thesis: ( ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) & ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) )
thus ( f is_left_ext_Riemann_integrable_on a,b implies f | A is_integrable_on L-Meas ) by A89; :: thesis: ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty )
thus ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = +infty ) by A1, A2, A3, A4, Lm7; :: thesis: verum

end;

end;