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_improper_integrable_on a,b & f | A is nonpositive holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,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_improper_integrable_on a,b & f | A is nonpositive holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,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_improper_integrable_on a,b & f | A is nonpositive implies ( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,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_improper_integrable_on a,b and
A4: f | A is nonpositive ; :: thesis: ( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = -infty ) )
reconsider A1 = A as Element of L-Field by A2, MEASUR10:5, MEASUR12:75;
A5: - f is_improper_integrable_on a,b by A1, A3, INTEGR24:62;
A6: improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) by A1, A3, INTEGR24:62;
- (f | A) is nonnegative by A4, Th5;
then A7: (- f) | A is nonnegative by RFUNCT_1:46;
A8: dom (- f) = dom f by VALUED_1:8;
then A9: improper_integral ((- f),a,b) = Integral (L-Meas,((- f) | A)) by A1, A2, A5, A7, Th45
.= Integral (L-Meas,(- (f | A))) by RFUNCT_1:46 ;
A10: dom (f | A) = A by A1, A2, RELAT_1:62;
then A1 = (dom f) /\ A1 by RELAT_1:61;
then A11: f | A is A1 -measurable by A1, A2, A3, Th35, MESFUNC6:76;
Integral (L-Meas,(- (f | A))) = - (Integral (L-Meas,(f | A))) by A10, A11, Th39;
hence improper_integral (f,a,b) = Integral (L-Meas,(f | A)) by A6, A9, XXREAL_3:10; :: thesis: ( ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = -infty ) )

hereby :: thesis: ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = -infty )

assume ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) ; :: thesis: f | A is_integrable_on L-Meas
then consider c being Real such that
A12: ( a < c & c < b ) and
A13: f is_left_ext_Riemann_integrable_on a,c and
A14: f is_right_ext_Riemann_integrable_on c,b ;
( ].a,c.] c= ].a,b.[ & [.c,b.[ c= ].a,b.[ ) by A12, XXREAL_1:49, XXREAL_1:48;
then A15: ( ].a,c.] c= dom f & [.c,b.[ c= dom f ) by A1;
then (- 1) (#) f is_left_ext_Riemann_integrable_on a,c by A13, INTEGR24:30;
then A16: - f is_left_ext_Riemann_integrable_on a,c by VALUED_1:def 6;
(- 1) (#) f is_right_ext_Riemann_integrable_on c,b by A14, A15, INTEGR24:31;
then - f is_right_ext_Riemann_integrable_on c,b by VALUED_1:def 6;
then (- f) | A is_integrable_on L-Meas by A1, A2, A8, A5, A7, A12, A16, Th45;
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 A17: for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ; :: thesis: Integral (L-Meas,(f | A)) = -infty
for c being Real st a < c & c < b & - f is_left_ext_Riemann_integrable_on a,c holds
not - f is_right_ext_Riemann_integrable_on c,b

proof

let c be Real; :: thesis: ( a < c & c < b & - f is_left_ext_Riemann_integrable_on a,c implies not - f is_right_ext_Riemann_integrable_on c,b )
assume A18: ( a < c & c < b ) ; :: thesis: ( not - f is_left_ext_Riemann_integrable_on a,c or not - f is_right_ext_Riemann_integrable_on c,b )

per cases ( not f is_left_ext_Riemann_integrable_on a,c or not f is_right_ext_Riemann_integrable_on c,b ) by A17, A18;

suppose A19: not f is_left_ext_Riemann_integrable_on a,c ; :: thesis: ( not - f is_left_ext_Riemann_integrable_on a,c or not - f is_right_ext_Riemann_integrable_on c,b )

].a,c.] c= ].a,b.[ by A18, XXREAL_1:49;
then A20: ].a,c.] c= dom (- f) by A1, A8;

now :: thesis: not - f is_left_ext_Riemann_integrable_on a,c

assume - f is_left_ext_Riemann_integrable_on a,c ; :: thesis: contradiction
then (- 1) (#) (- f) is_left_ext_Riemann_integrable_on a,c by A20, INTEGR24:30;
hence contradiction by A19; :: thesis: verum

end;

hence ( not - f is_left_ext_Riemann_integrable_on a,c or not - f is_right_ext_Riemann_integrable_on c,b ) ; :: thesis: verum

end;

suppose A21: not f is_right_ext_Riemann_integrable_on c,b ; :: thesis: ( not - f is_left_ext_Riemann_integrable_on a,c or not - f is_right_ext_Riemann_integrable_on c,b )

[.c,b.[ c= ].a,b.[ by A18, XXREAL_1:48;
then A22: [.c,b.[ c= dom (- f) by A1, A8;

now :: thesis: not - f is_right_ext_Riemann_integrable_on c,b

assume - f is_right_ext_Riemann_integrable_on c,b ; :: thesis: contradiction
then (- 1) (#) (- f) is_right_ext_Riemann_integrable_on c,b by A22, INTEGR24:31;
hence contradiction by A21; :: thesis: verum

end;

hence ( not - f is_left_ext_Riemann_integrable_on a,c or not - f is_right_ext_Riemann_integrable_on c,b ) ; :: thesis: verum

end;

end;

end;

then Integral (L-Meas,((- f) | A)) = +infty by A1, A8, A2, A5, A7, Th45;
then Integral (L-Meas,(- (f | A))) = +infty by RFUNCT_1:46;
then - (Integral (L-Meas,(f | A))) = +infty by A10, A11, Th39;
hence Integral (L-Meas,(f | A)) = -infty by XXREAL_3:23; :: thesis: verum

end;