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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 f being PartFunc of X,ExtREAL st E c= dom f & f is E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 E -measurable & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) 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 E -measurable and
A3: E = {} and
A4: for n being Nat holds F . n is_simple_func_in S ; :: 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 )
take I = NAT --> 0.; :: thesis: ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
A5: M . E = 0 by A3, VALUED_0:def 19;
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))
reconsider m = n as Element of NAT by ORDINAL1:def 12;
reconsider D = dom (F . m) as Element of S by A4, MESFUNC5:37;
F . m is D -measurable by A4, MESFUNC2:34;
then Integral (M,((F . m) | E)) = 0 by A5, MESFUNC5:94;
hence I . n = Integral (M,((F . n) | E)) by FUNCOP_1:7; :: thesis: verum

end;

defpred S₁[ Nat] means (Partial_Sums I) . $1 = 0 ;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: I . (k + 1) = 0 by FUNCOP_1:7;
(Partial_Sums I) . (k + 1) = ((Partial_Sums I) . k) + (I . (k + 1)) by Def1;
hence S₁[k + 1] by A7, A8; :: thesis: verum

end;

(Partial_Sums I) . 0 = I . 0 by Def1;
then A9: S₁[ 0 ] by FUNCOP_1:7;
A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A6);
A11: for n being Nat holds (Partial_Sums I) . n = 0 by A10;
then A12: lim (Partial_Sums I) = 0 by MESFUNC5:52;
Partial_Sums I is convergent_to_finite_number by A11, MESFUNC5:52;
then Partial_Sums I is convergent ;
hence I is summable ; :: thesis: Integral (M,(f | E)) = Sum I
A13: E = dom (f | E) by A1, RELAT_1:62;
then E = (dom f) /\ E by RELAT_1:61;
then Integral (M,((f | E) | E)) = 0 by A2, A5, A13, MESFUNC5:42, MESFUNC5:94;
hence Integral (M,(f | E)) = Sum I by A12; :: thesis: verum