let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
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:
take I = NAT --> 0.; :: thesis:
A5: M . E = 0 by A3, VALUED_0:def 19;
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis:

let n be Nat; :: thesis:
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:

end;

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

let k be Nat; :: thesis:
assume A7: S₁[k] ; :: thesis:
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:

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