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 ;
now :: thesis: for n being Nat holds (- F) . n is V120()
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;
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) )
proof
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 ;
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;
A9: for x being Element of X st x in E holds
( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )
proof
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 ;
hence (- f) . x = Sum ((- F) # x) by ; :: thesis: verum
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 ;
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 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 ;
(- F) . n = - (F . n) by Th37;
then F . n = - ((- F) . n) by Th36;
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: Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by A1, A3, Th55;
Partial_Sums J is convergent by ;
then lim (- ()) = - (lim ()) by DBLSEQ_3:17
.= - (Integral (M,((- f) | E))) by ;
then lim () = - (Integral (M,((- f) | E))) by Th44;
hence Integral (M,(f | E)) = Sum I by ; :: thesis: verum