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 nonpositive 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 nonpositive 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 nonpositive 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 nonpositive ; :: 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 ) )
A5: a < b by A2, XXREAL_1:26;
- (f | A) is nonnegative by A4, Th5;
then A6: (- f) | A is nonnegative by RFUNCT_1:46;
A7: dom (- f) = dom f by VALUED_1:8;
A8: - f is_left_improper_integrable_on a,b by A3, A5, A1, INTEGR24:55;
then left_improper_integral ((- f),a,b) = Integral (L-Meas,((- f) | A)) by A1, A7, A2, A6, Th43;
then - (left_improper_integral (f,a,b)) = Integral (L-Meas,((- f) | A)) by A3, A5, A1, INTEGR24:55;
then A9: left_improper_integral (f,a,b) = - (Integral (L-Meas,((- f) | A))) ;
reconsider A1 = A as Element of L-Field by A2, MEASUR10:5, MEASUR12:75;
A10: A1 = dom (f | A) by A1, A2, RELAT_1:62;
then A11: A1 = (dom f) /\ A1 by RELAT_1:61;
A12: dom (R_EAL (f | A)) = A1 by A10, MESFUNC5:def 7;
f is A1 -measurable by A1, A2, A3, Th34;
then A13: R_EAL (f | A) is A1 -measurable by A11, MESFUNC6:def 1, MESFUNC6:76;
A14: R_EAL ((- f) | A) = R_EAL (- (f | A)) by RFUNCT_1:46
.= - (R_EAL (f | A)) by MESFUNC6:28 ;
A15: Integral (L-Meas,((- f) | A)) = Integral (L-Meas,(- (R_EAL (f | A)))) by A14, MESFUNC6:def 3
.= - (Integral (L-Meas,(R_EAL (f | A)))) by A12, A13, MESFUN11:52
.= - (Integral (L-Meas,(f | A))) by MESFUNC6:def 3 ;
hence left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A9; :: 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 ) )

hereby :: thesis: ( not f is_left_ext_Riemann_integrable_on a,b implies Integral (L-Meas,(f | A)) = -infty )

assume f is_left_ext_Riemann_integrable_on a,b ; :: thesis: f | A is_integrable_on L-Meas
then (- 1) (#) f is_left_ext_Riemann_integrable_on a,b by A1, INTEGR24:30;
then - f is_left_ext_Riemann_integrable_on a,b by VALUED_1:def 6;
then (- f) | A is_integrable_on L-Meas by A7, A1, A2, A8, A6, Th43;
then - (f | A) is_integrable_on L-Meas by RFUNCT_1:46;
then (- 1) (#) (- (f | A)) is_integrable_on L-Meas by MESFUNC6:102;
hence f | A is_integrable_on L-Meas ; :: thesis: verum

end;

hereby :: thesis: verum

assume not f is_left_ext_Riemann_integrable_on a,b ; :: thesis: Integral (L-Meas,(f | A)) = -infty
then A16: ( Integral (L-Meas,(f | A)) = +infty or Integral (L-Meas,(f | A)) = -infty ) by A15, A9, A3, INTEGR24:34;
R_EAL (f | A) is nonpositive by A4, MESFUNC5:def 7;
then Integral (L-Meas,(R_EAL (f | A))) <= 0 by A13, A12, MESFUN11:61;
hence Integral (L-Meas,(f | A)) = -infty by A16, MESFUNC6:def 3; :: thesis: verum

end;