let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 Functional_Sequence of X,ExtREAL; :: 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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) implies 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 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: 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;

set G = - F;

A6: E c= dom (- f) by A1, MESFUNC1:def 7;

A8: for n being Nat holds

( (- F) . n is_simple_func_in S & (- F) . n is nonnegative & E c= dom ((- F) . n) )

( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )

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: ( ( 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: 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: verum

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 F being Functional_Sequence of X,ExtREAL

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 Functional_Sequence of X,ExtREAL; :: 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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

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 & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) implies 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 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: 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;

set G = - F;

A6: E c= dom (- f) by A1, MESFUNC1:def 7;

now :: thesis: for n being Nat holds (- F) . n is V120()

then A7:
- F is additive
by Th47;let n be Nat; :: thesis: (- F) . n is V120()

F . n is nonpositive by A4;

then - (F . n) is V120() ;

hence (- F) . n is V120() by Th37; :: thesis: verum

end;F . n is nonpositive by A4;

then - (F . n) is V120() ;

hence (- F) . n is V120() by Th37; :: thesis: verum

A8: for n being Nat holds

( (- F) . n is_simple_func_in S & (- F) . n is nonnegative & E c= dom ((- F) . n) )

proof

A9:
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 nonnegative & E c= dom ((- F) . n) )

(- 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 nonnegative & E c= dom ((- F) . n) )

F . n is nonpositive by A4;

then - (F . n) is nonnegative ;

hence (- F) . n is nonnegative by Th37; :: thesis: E c= dom ((- F) . n)

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

end;(- 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 nonnegative & E c= dom ((- F) . n) )

F . n is nonpositive by A4;

then - (F . n) is nonnegative ;

hence (- F) . n is nonnegative by Th37; :: thesis: E c= dom ((- F) . n)

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

( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )

proof

consider J being ExtREAL_sequence such that
let x be Element of X; :: thesis: ( x in E implies ( (- F) # x is summable & (- f) . x = Sum ((- F) # x) ) )

assume A10: x in E ; :: thesis: ( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )

then A11: ( F # x is summable & f . x = Sum (F # x) ) by A5;

hence (- F) # x is summable by Th48; :: thesis: (- f) . x = Sum ((- F) # x)

(- f) . x = - (f . x) by A6, A10, MESFUNC1:def 7;

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

end;assume A10: x in E ; :: thesis: ( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )

then A11: ( F # x is summable & f . x = Sum (F # x) ) by A5;

hence (- F) # x is summable by Th48; :: thesis: (- f) . x = Sum ((- F) # x)

(- f) . x = - (f . x) by A6, A10, MESFUNC1:def 7;

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

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: ( ( 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 A12, 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 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: verum

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

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