let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: 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 ; :: thesis:
set g = - f;
A4: E c= dom (- f) by A1, MESFUNC1:def 7;
then consider G being Functional_Sequence of X,ExtREAL such that
A5: ( G is additive & ( for n being Nat holds
( G . n is_simple_func_in S & G . n is nonnegative & G . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( G # x is summable & (- f) . x = Sum (G # x) ) ) & ex J being ExtREAL_sequence st
( ( for n being Nat holds J . n = Integral (M,((G . n) | E)) ) & J is summable & Integral (M,((- f) | E)) = Sum J ) ) by A1, A2, A3, MESFUNC9:48, MEASUR11:63;
take F = - G; :: thesis:
thus F is additive by A5, Th41; :: thesis:
thus for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) :: thesis:

end;

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

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

end;

thus ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) :: thesis:

consider J being ExtREAL_sequence such that
A9: ( ( for n being Nat holds J . n = Integral (M,((G . n) | E)) ) & J is summable & Integral (M,((- f) | E)) = Sum J ) by A5;
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 A10: n in dom I by ORDINAL1:def 12;
A11: J . n = Integral (M,((G . n) | E)) by A9;
F . n = - (G . n) by Th37;
then A12: (F . n) | E = - ((G . n) | E) by Th3;
A13: G . n is_simple_func_in S by A5;
then consider GG being Finite_Sep_Sequence of S such that
A14: ( dom (G . n) = union (rng GG) & ( for k being Nat
for x, y being Element of X st k in dom GG & x in GG . k & y in GG . k holds
(G . n) . x = (G . n) . y ) ) by MESFUNC2:def 4;
reconsider V = union (rng GG) as Element of S by MESFUNC2:31;
reconsider VE = V /\ E as Element of S ;
A15: VE = dom ((G . n) | E) by A14, RELAT_1:61;
(G . n) | E is VE -measurable by A13, MESFUNC2:34, MESFUNC5:34;
then Integral (M,((F . n) | E)) = - (Integral (M,((G . n) | E))) by A12, A15, Th52;
hence I . n = Integral (M,((F . n) | E)) by A10, A11, MESFUNC1:def 7; :: thesis:

end;

end;