let f be PartFunc of REAL,REAL; :: thesis: for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonpositive holds
( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) )
let a be Real; :: thesis: for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonpositive holds
( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) )
let A be non empty Subset of REAL; :: thesis: ( right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & f is nonpositive implies ( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) ) )
assume that
A1: right_closed_halfline a c= dom f and
A2: A = right_closed_halfline a and
A3: f is_+infty_improper_integrable_on a and
A4: f is nonpositive ; :: thesis: ( improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) & ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) )
A5: A = [.a,+infty.[ by A2, LIMFUNC1:def 2;
then reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;
A6: - f is_+infty_improper_integrable_on a by A1, A3, INTEGR25:44;
A7: improper_integral_+infty ((- f),a) = - (improper_integral_+infty (f,a)) by A1, A3, INTEGR25:44;
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),a) = Integral (L-Meas,((- f) | A)) by A1, A2, A6, A9, Th49
.= Integral (L-Meas,(- (f | A))) by RFUNCT_1:46 ;
A12: dom (f | A) = A by A1, A2, RELAT_1:62;
then A1 = (dom f) /\ A1 by RELAT_1:61;
then A13: f | A is A1 -measurable by A1, A2, A3, A5, Th36, MESFUNC6:76;
then Integral (L-Meas,(- (f | A))) = - (Integral (L-Meas,(f | A))) by A12, Th39;
hence improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) by A7, A11, XXREAL_3:10; :: thesis: ( ( f is_+infty_ext_Riemann_integrable_on a implies f | A is_integrable_on L-Meas ) & ( not f is_+infty_ext_Riemann_integrable_on a implies Integral (L-Meas,(f | A)) = -infty ) )

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

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

now :: thesis: not - f is_+infty_ext_Riemann_integrable_on a

assume - f is_+infty_ext_Riemann_integrable_on a ; :: thesis: contradiction
then (- 1) (#) (- f) is_+infty_ext_Riemann_integrable_on a by A1, A10, INTEGR10:9;
hence contradiction by A14; :: thesis: verum

end;

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

end;