let f be PartFunc of REAL,REAL; :: thesis: for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonpositive holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )
let b be Real; :: thesis: for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonpositive holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )
let A be non empty Subset of REAL; :: thesis: ( left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonpositive implies ( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: A = left_closed_halfline b and
A3: f is_-infty_improper_integrable_on b and
A4: f is nonpositive ; :: thesis: ( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )
A5: A = ].-infty,b.] by A2, LIMFUNC1:def 1;
then reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;
A6: - f is_-infty_improper_integrable_on b by A1, A3, INTEGR25:43;
A7: improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b)) by A1, A3, INTEGR25:43;
for x being object st x in dom (- f) holds
0 <= (- f) . x

proof

let x be object ; :: thesis: ( x in dom (- f) implies 0 <= (- f) . x )
assume x in dom (- f) ; :: thesis: 0 <= (- f) . x
then A8: f . x <= 0 by A4, MESFUNC6:53;
(- f) . x = - (f . x) by VALUED_1:8;
hence 0 <= (- f) . x by A8; :: thesis: verum

end;

then A9: - f is nonnegative by MESFUNC6:52;
A10: dom (- f) = dom f by VALUED_1:8;
then A11: improper_integral_-infty ((- f),b) = Integral (L-Meas,((- f) | A)) by A1, A2, A6, A9, Th47
.= Integral (L-Meas,(- (f | A))) by RFUNCT_1:46 ;
A12: dom (f | A) = A by A1, A2, RELAT_1:62;
then A13: A1 = (dom f) /\ A1 by RELAT_1:61;
A14: f | A is A1 -measurable by A13, A1, A2, A3, A5, Th37, MESFUNC6:76;
then Integral (L-Meas,(- (f | A))) = - (Integral (L-Meas,(f | A))) by A12, Th39;
hence improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) by A7, A11, XXREAL_3:10; :: thesis: ( ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )

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

assume f is_-infty_ext_Riemann_integrable_on b ; :: thesis: f | A is_integrable_on L-Meas
then (- 1) (#) f is_-infty_ext_Riemann_integrable_on b by A1, INTEGR10:11;
then - f is_-infty_ext_Riemann_integrable_on b by VALUED_1:def 6;
then (- f) | A is_integrable_on L-Meas by A1, A2, A6, A10, A9, Th47;
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 A15: not f is_-infty_ext_Riemann_integrable_on b ; :: thesis: Integral (L-Meas,(f | A)) = -infty

now :: thesis: not - f is_-infty_ext_Riemann_integrable_on b

assume - f is_-infty_ext_Riemann_integrable_on b ; :: thesis: contradiction
then (- 1) (#) (- f) is_-infty_ext_Riemann_integrable_on b by A1, A10, INTEGR10:11;
hence contradiction by A15; :: thesis: verum

end;

then Integral (L-Meas,((- f) | A)) = +infty by A1, A2, A6, A10, A9, Th47;
then Integral (L-Meas,(- (f | A))) = +infty by RFUNCT_1:46;
then - (Integral (L-Meas,(f | A))) = +infty by A12, A14, Th39;
hence Integral (L-Meas,(f | A)) = -infty by XXREAL_3:23; :: thesis: verum

end;