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
A0: E c= dom f and
B2: f is_measurable_on E and
A1: E = {} and
A2: for n being Nat holds F . n is_simple_func_in S ; :: thesis:
take I = NAT --> 0. ; :: thesis:
A5: M . E = 0 by A1, 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 13;
reconsider D = dom (F . m) as Element of S by A2, MESFUNC5:43;
F . m is_measurable_on D by A2, MESFUNC2:37;
then Integral M,((F . m) | E) = 0 by A5, MESFUNC5:100;
hence I . n = Integral M,((F . n) | E) by FUNCOP_1:13; :: thesis:

end;

defpred S₁[ Element of NAT ] means (Partial_Sums I) . $1 = 0 ;
(Partial_Sums I) . 0 = I . 0 by Def1;
then P1: S₁[ 0 ] by FUNCOP_1:13;
P2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume P21: S₁[k] ; :: thesis:
P22: I . (k + 1) = 0 by FUNCOP_1:13;
(Partial_Sums I) . (k + 1) = ((Partial_Sums I) . k) + (I . (k + 1)) by Def1;
then (Partial_Sums I) . (k + 1) = 0 + 0 by P21, P22;
hence S₁[k + 1] ; :: thesis:

end;

P3: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P1, P2);
for n being Nat holds (Partial_Sums I) . n = 0

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 13;
hence (Partial_Sums I) . n = 0 by P3; :: thesis:

end;

then A6: ( Partial_Sums I is convergent_to_finite_number & lim (Partial_Sums I) = 0 ) by MESFUNC5:58;
then Partial_Sums I is convergent by MESFUNC5:def 11;
hence I is summable by Def2; :: thesis:
A7: E = dom (f | E) by A0, RELAT_1:91;
then E = (dom f) /\ E by RELAT_1:90;
then Integral M,((f | E) | E) = 0 by A7, A5, B2, MESFUNC5:48, MESFUNC5:100;
hence Integral M,(f | E) = Sum I by A6, FUNCT_1:82; :: thesis: