let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
let E be Element of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: E c= dom f and
A2: f is nonpositive and
A3: f is E -measurable and
A4: for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) and
A5: for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ; :: thesis:
set g = - f;
set G = - F;
A6: E c= dom (- f) by A1, MESFUNC1:def 7;

let n be Nat; :: thesis:
F . n is nonpositive by A4;
then - (F . n) is without-infty ;
hence (- F) . n is without-infty by Th37; :: thesis:

end;

then A7: - F is additive by Th47;
A8: for n being Nat holds
( (- F) . n is_simple_func_in S & (- F) . n is nonnegative & E c= dom ((- F) . n) )

let n be Nat; :: thesis:
(- 1) (#) (F . n) is_simple_func_in S by A4, MESFUNC5:39;
then - (F . n) is_simple_func_in S by MESFUNC2:9;
hence (- F) . n is_simple_func_in S by Th37; :: thesis:
F . n is nonpositive by A4;
then - (F . n) is nonnegative ;
hence (- F) . n is nonnegative by Th37; :: thesis:
E c= dom (F . n) by A4;
then E c= dom (- (F . n)) by MESFUNC1:def 7;
hence E c= dom ((- F) . n) by Th37; :: thesis:

end;

A9: for x being Element of X st x in E holds
( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )

let x be Element of X; :: thesis:
assume A10: x in E ; :: thesis:
then A11: ( F # x is summable & f . x = Sum (F # x) ) by A5;
hence (- F) # x is summable by Th48; :: thesis:
(- f) . x = - (f . x) by A6, A10, MESFUNC1:def 7;
hence (- f) . x = Sum ((- F) # x) by A11, Th48; :: thesis:

end;

consider J being ExtREAL_sequence such that
A12: ( ( for n being Nat holds J . n = Integral (M,(((- F) . n) | E)) ) & J is summable & Integral (M,((- f) | E)) = Sum J ) by A2, A1, A3, A6, A7, A8, A9, MESFUNC9:47, MEASUR11:63;
take I = - J; :: thesis:
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis:

let n be Nat; :: thesis:
dom I = NAT by FUNCT_2:def 1;
then n in dom I by ORDINAL1:def 12;
then I . n = - (J . n) by MESFUNC1:def 7;
then A13: I . n = - (Integral (M,(((- F) . n) | E))) by A12;
A14: E c= dom ((- F) . n) by A8;
A15: (- F) . n is E -measurable by A8, MESFUNC2:34;
(- F) . n = - (F . n) by Th37;
then F . n = - ((- F) . n) by Th36;
hence I . n = Integral (M,((F . n) | E)) by A13, A14, A15, Th55; :: thesis:

end;

thus I is summable by A12, Th45; :: thesis:
A16: Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by A1, A3, Th55;
Partial_Sums J is convergent by A12, MESFUNC9:def 2;
then lim (- (Partial_Sums J)) = - (lim (Partial_Sums J)) by DBLSEQ_3:17
.= - (Integral (M,((- f) | E))) by A12, MESFUNC9:def 3 ;
then lim (Partial_Sums I) = - (Integral (M,((- f) | E))) by Th44;
hence Integral (M,(f | E)) = Sum I by A16, MESFUNC9:def 3; :: thesis: