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 nonnegative and
A3: f is E -measurable and
A4: F is additive and
A5: E common_on_dom F and
A6: for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative ) and
A7: for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ; :: thesis:
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (F . $1) | E;
consider g1 being Functional_Sequence of X,ExtREAL such that
A8: for n being Nat holds g1 . n = H₁(n) from SEQFUNC:sch 1();
A9: for n being Nat holds
( (F . n) | E is_simple_func_in S & (F . n) | E is nonnegative & dom ((F . n) | E) = E )

let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
thus (F . n) | E is_simple_func_in S by A6, MESFUNC5:34; :: thesis:
thus (F . n) | E is nonnegative by A6, MESFUNC5:15; :: thesis:
E c= dom (F . n9) by A5, SEQFUNC:def 9;
hence dom ((F . n) | E) = E by RELAT_1:62; :: thesis:

end;

for n, m being Nat holds dom (g1 . n) = dom (g1 . m)

let n, m be Nat; :: thesis:
dom (g1 . m) = dom ((F . m) | E) by A8;
then A10: dom (g1 . m) = E by A9;
dom (g1 . n) = dom ((F . n) | E) by A8;
hence dom (g1 . n) = dom (g1 . m) by A9, A10; :: thesis:

end;

then A11: g1 is with_the_same_dom ;
set G = Partial_Sums g1;
deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral (M,(g1 . $1));
consider I being ExtREAL_sequence such that
A12: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
take I ; :: thesis:
A13: dom (f | E) = E by A1, RELAT_1:62;
then (dom f) /\ E = E by RELAT_1:61;
then A14: f | E is E -measurable by A3, MESFUNC5:42;
set L = Partial_Sums I;
A15: for n being Nat holds I . n = Integral (M,((F . n) | E))

let n be Nat; :: thesis:
reconsider m = n as Element of NAT by ORDINAL1:def 12;
I . m = Integral (M,(g1 . m)) by A12;
hence I . n = Integral (M,((F . n) | E)) by A8; :: thesis:

end;

A16: for k being Nat holds g1 . k is nonnegative

let k be Nat; :: thesis:
(F . k) | E is nonnegative by A9;
hence g1 . k is nonnegative by A8; :: thesis:

end;

A17: for n being Nat holds
( (Partial_Sums g1) . n is_simple_func_in S & (Partial_Sums g1) . n is nonnegative & dom ((Partial_Sums g1) . n) = E )

let n be Nat; :: thesis:
A18: for n being Nat holds g1 . n is_simple_func_in S

let n be Nat; :: thesis:
(F . n) | E is_simple_func_in S by A9;
hence g1 . n is_simple_func_in S by A8; :: thesis:

end;

hence (Partial_Sums g1) . n is_simple_func_in S by Th35; :: thesis:
thus (Partial_Sums g1) . n is nonnegative by A16, Th36; :: thesis:
dom (g1 . 0) = dom ((F . 0) | E) by A8;
then dom (g1 . 0) = E by A9;
hence dom ((Partial_Sums g1) . n) = E by A11, A18, Th29, Th35; :: thesis:

end;

(Partial_Sums g1) . 0 = g1 . 0 by Def4;
then A19: (Partial_Sums g1) . 0 = (F . 0) | E by A8;
A20: for n being Nat holds integral' (M,((Partial_Sums g1) . n)) = (Partial_Sums I) . n

defpred S₁[ Nat] means (Partial_Sums I) . $1 = integral' (M,((Partial_Sums g1) . $1));
let n be Nat; :: thesis:
A21: (Partial_Sums g1) . 0 is nonnegative by A17;
A22: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A23: S₁[k] ; :: thesis:
(Partial_Sums I) . (k + 1) = ((Partial_Sums I) . k) + (I . (k + 1)) by Def1;
then A24: (Partial_Sums I) . (k + 1) = (integral' (M,((Partial_Sums g1) . k))) + (Integral (M,((F . (k + 1)) | E))) by A15, A23;
A25: (F . (k + 1)) | E is_simple_func_in S by A9;
A26: dom ((F . (k + 1)) | E) = E by A9;
A27: (Partial_Sums g1) . k is_simple_func_in S by A17;
(Partial_Sums g1) . (k + 1) = ((Partial_Sums g1) . k) + (g1 . (k + 1)) by Def4;
then A28: (Partial_Sums g1) . (k + 1) = ((Partial_Sums g1) . k) + ((F . (k + 1)) | E) by A8;
A29: (F . (k + 1)) | E is nonnegative by A9;
A30: (Partial_Sums g1) . k is nonnegative by A17;
A31: dom ((Partial_Sums g1) . k) = E by A17;
then E = (dom ((Partial_Sums g1) . k)) /\ (dom ((F . (k + 1)) | E)) by A26;
then dom (((Partial_Sums g1) . k) + ((F . (k + 1)) | E)) = E by A25, A29, A27, A30, MESFUNC5:65;
then A32: integral' (M,(((Partial_Sums g1) . k) + ((F . (k + 1)) | E))) = (integral' (M,(((Partial_Sums g1) . k) | E))) + (integral' (M,(((F . (k + 1)) | E) | E))) by A25, A29, A27, A30, MESFUNC5:65;
((Partial_Sums g1) . k) | E = (Partial_Sums g1) . k by A31;
hence S₁[k + 1] by A28, A24, A25, A29, A32, MESFUNC5:89; :: thesis:

end;

(Partial_Sums I) . 0 = I . 0 by Def1;
then A33: (Partial_Sums I) . 0 = Integral (M,((Partial_Sums g1) . 0)) by A15, A19;
(Partial_Sums g1) . 0 is_simple_func_in S by A17;
then A34: S₁[ 0 ] by A33, A21, MESFUNC5:89;
A35: for k being Nat holds S₁[k] from NAT_1:sch 2(A34, A22);
thus integral' (M,((Partial_Sums g1) . n)) = (Partial_Sums I) . n by A35; :: thesis:

end;

g1 . 0 = (F . 0) | E by A8;
then A36: dom (g1 . 0) = E by A9;
A37: for x being Element of X st x in dom (f | E) holds
( g1 # x is summable & (f | E) . x = Sum (g1 # x) )

let x be Element of X; :: thesis:
assume A38: x in dom (f | E) ; :: thesis:
then A39: f . x = (f | E) . x by FUNCT_1:47;
A40: for n being object st n in NAT holds
(F # x) . n = (g1 # x) . n

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n1 = n as Nat ;
A41: (F # x) . n = (F . n1) . x by MESFUNC5:def 13;
A42: dom ((F . n1) | E) = E by A9;
(F . n1) | E = g1 . n1 by A8;
then (g1 . n1) . x = (F . n1) . x by A13, A38, A42, FUNCT_1:47;
hence (F # x) . n = (g1 # x) . n by A41, MESFUNC5:def 13; :: thesis:

end;

A43: f . x = Sum (F # x) by A7, A13, A38;
F # x is summable by A7, A13, A38;
hence ( g1 # x is summable & (f | E) . x = Sum (g1 # x) ) by A43, A39, A40, FUNCT_2:12; :: thesis:

end;

A44: f | E is nonnegative by A2, MESFUNC5:15;
then consider F being Functional_Sequence of X,ExtREAL, K being ExtREAL_sequence such that
A45: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | E) ) and
A46: for n being Nat holds F . n is nonnegative and
A47: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | E) holds
(F . n) . x <= (F . m) . x and
A48: for x being Element of X st x in dom (f | E) holds
( F # x is convergent & lim (F # x) = (f | E) . x ) and
A49: for n being Nat holds K . n = integral' (M,(F . n)) and
K is convergent and
A50: integral+ (M,(f | E)) = lim K by A13, A14, MESFUNC5:def 15;
A51: g1 is additive by A4, A8, Th31;
A52: for x being Element of X st x in E holds
( F # x is convergent & (Partial_Sums g1) # x is convergent & lim (F # x) = lim ((Partial_Sums g1) # x) )

let x be Element of X; :: thesis:
assume A53: x in E ; :: thesis:
hence F # x is convergent by A13, A48; :: thesis:
g1 # x is summable by A13, A37, A53;
then Partial_Sums (g1 # x) is convergent ;
hence (Partial_Sums g1) # x is convergent by A11, A51, A36, A53, Th33; :: thesis:
A54: (f | E) . x = Sum (g1 # x) by A13, A37, A53;
g1 # x is summable by A13, A37, A53;
then lim ((Partial_Sums g1) # x) = (f | E) . x by A4, A13, A8, A11, A36, A53, A54, Th31, Th34;
hence lim (F # x) = lim ((Partial_Sums g1) # x) by A13, A48, A53; :: thesis:

end;

A55: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
((Partial_Sums g1) . n) . x <= ((Partial_Sums g1) . m) . x by A11, A16, A36, Th37;
then A56: Partial_Sums I is convergent by A13, A17, A20, A45, A46, A47, A49, A52, MESFUNC5:76;
lim (Partial_Sums I) = integral+ (M,(f | E)) by A13, A17, A20, A45, A46, A47, A49, A50, A55, A52, MESFUNC5:76;
hence ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) by A13, A15, A14, A44, A56, MESFUNC5:88; :: thesis: