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 nonpositive 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 nonpositive 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 nonpositive 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 nonpositive ; :: 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 ) )
- (f | A) is nonnegative by A4, Th5;
then A5: (- f) | A is nonnegative by RFUNCT_1:46;
A6: dom (- f) = dom f by VALUED_1:8;
A7: a < b by A2, XXREAL_1:27;
then A8: - f is_right_improper_integrable_on a,b by A3, A1, INTEGR24:56;
then right_improper_integral ((- f),a,b) = Integral (L-Meas,((- f) | A)) by A1, A6, A2, A5, Th41;
then - (right_improper_integral (f,a,b)) = Integral (L-Meas,((- f) | A)) by A3, A7, A1, INTEGR24:56;
then A9: right_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, Th33;
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 right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A9; :: 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 ) )

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

assume f is_right_ext_Riemann_integrable_on a,b ; :: thesis: f | A is_integrable_on L-Meas
then (- 1) (#) f is_right_ext_Riemann_integrable_on a,b by A1, INTEGR24:31;
then - f is_right_ext_Riemann_integrable_on a,b by VALUED_1:def 6;
then (- f) | A is_integrable_on L-Meas by A6, A1, A2, A8, A5, Th41;
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_right_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 A9, A15, A3, INTEGR24:39;
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;