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 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: ( 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 A5, Th41; :: 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 ) )

( 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 )

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

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 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: ( 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 A5, Th41; :: 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

thus
for x being Element of X st x in E holds
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 A5, MESFUNC5:39;

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 A6, MESFUNC2:34; :: thesis: verum

end;(- 1) (#) (G . n) is_simple_func_in S by A5, MESFUNC5:39;

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 A6, MESFUNC2:34; :: thesis: verum

( 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

thus
ex I being ExtREAL_sequence st
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 A7, A4, MESFUNC1:def 7;

then f . x = - (Sum (G # x)) by A8;

hence f . x = Sum (F # x) by A8, Th48; :: thesis: verum

end;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 A7, A4, MESFUNC1:def 7;

then f . x = - (Sum (G # x)) by A8;

hence f . x = Sum (F # x) by A8, Th48; :: thesis: verum

( ( 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 )

A16: Partial_Sums J is convergent by A9, MESFUNC9:def 2;

A17: Sum I = lim (Partial_Sums I) by MESFUNC9:def 3

.= lim (- (Partial_Sums J)) by Th44

.= - (lim (Partial_Sums J)) by A16, DBLSEQ_3:17

.= - (Integral (M,((- f) | E))) by A9, MESFUNC9:def 3 ;

A18: dom (f | E) = E by A1, RELAT_1:62;

A19: E = (dom f) /\ E by A1, XBOOLE_1:28;

(- f) | E = - (f | E) by Th3;

then Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by A3, A18, A19, Th52, MESFUNC5:42;

hence Integral (M,(f | E)) = Sum I by A17; :: thesis: verum

end;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

thus
I is summable
by A9, Th45; :: thesis: Integral (M,(f | E)) = Sum I
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 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: verum

end;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: verum

A16: Partial_Sums J is convergent by A9, MESFUNC9:def 2;

A17: Sum I = lim (Partial_Sums I) by MESFUNC9:def 3

.= lim (- (Partial_Sums J)) by Th44

.= - (lim (Partial_Sums J)) by A16, DBLSEQ_3:17

.= - (Integral (M,((- f) | E))) by A9, MESFUNC9:def 3 ;

A18: dom (f | E) = E by A1, RELAT_1:62;

A19: E = (dom f) /\ E by A1, XBOOLE_1:28;

(- f) | E = - (f | E) by Th3;

then Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by A3, A18, A19, Th52, MESFUNC5:42;

hence Integral (M,(f | E)) = Sum I by A17; :: thesis: verum