let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

let f be PartFunc of X,ExtREAL; :: thesis: ( E c= dom f & f is nonpositive & f is E -measurable implies ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) ) )

assume that
A1: E c= dom f and
A2: f is nonpositive and
A3: f is E -measurable ; :: thesis: ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

set g = - f;
A4: E c= dom (- f) by ;
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 ;
take F = - G; :: thesis: ( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

thus F is additive by ; :: thesis: ( ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )

thus for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) :: thesis: ( ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & 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 ) )
proof
let n be Nat; :: thesis: ( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable )
(- 1) (#) (G . n) is_simple_func_in S by ;
then - (G . n) is_simple_func_in S by MESFUNC2:9;
hence A6: F . n is_simple_func_in S by Th37; :: thesis: ( F . n is nonpositive & F . n is E -measurable )
G . n is nonnegative by A5;
then - (G . n) is nonpositive ;
hence F . n is nonpositive by Th37; :: thesis: F . n is E -measurable
thus F . n is E -measurable by ; :: thesis: verum
end;
thus for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) :: thesis: 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 )
proof
let x be Element of X; :: thesis: ( x in E implies ( F # x is summable & f . x = Sum (F # x) ) )
assume A7: x in E ; :: thesis: ( F # x is summable & f . x = Sum (F # x) )
then A8: ( G # x is summable & (- f) . x = Sum (G # x) ) by A5;
hence F # x is summable by Th48; :: thesis: f . x = Sum (F # x)
(- f) . x = - (f . x) by ;
then f . x = - (Sum (G # x)) by A8;
hence f . x = Sum (F # x) by ; :: thesis: verum
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: verum
proof
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: ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis: ( I is summable & Integral (M,(f | E)) = Sum I )
proof
let n be Nat; :: thesis: I . n = Integral (M,((F . n) | E))
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 ;
(G . n) | E is VE -measurable by ;
then Integral (M,((F . n) | E)) = - (Integral (M,((G . n) | E))) by ;
hence I . n = Integral (M,((F . n) | E)) by ; :: thesis: verum
end;
thus I is summable by ; :: thesis: Integral (M,(f | E)) = Sum I
A16: Partial_Sums J is convergent by ;
A17: Sum I = lim () by MESFUNC9:def 3
.= lim (- ()) by Th44
.= - (lim ()) by
.= - (Integral (M,((- f) | E))) by ;
A18: dom (f | E) = E by ;
A19: E = (dom f) /\ E by ;
(- f) | E = - (f | E) by Th3;
then Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by ;
hence Integral (M,(f | E)) = Sum I by A17; :: thesis: verum
end;