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 st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums 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 st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums 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 st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let E be Element of S; :: thesis: ( E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I ) )
assume that
A1: E c= dom (F . 0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) and
A5: for x being Element of X st x in E holds
F # x is summable ; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
set G = - F;
(- F) . 0 = - (F . 0) by Th37;
then A6: E c= dom ((- F) . 0) by A1, MESFUNC1:def 7;
A7: - F is additive by A2, Th41;
A8: - F is with_the_same_dom by A3, Th40;
A9: for n being Nat holds
( (- F) . n is nonnegative & (- F) . n is E -measurable )

proof

let n be Nat; :: thesis: ( (- F) . n is nonnegative & (- F) . n is E -measurable )
F . n is nonpositive by A4;
then - (F . n) is nonnegative ;
hence (- F) . n is nonnegative by Th37; :: thesis: (- F) . n is E -measurable
E c= dom (F . n) by A1, A3, MESFUNC8:def 2;
then - (F . n) is E -measurable by A4, MEASUR11:63;
hence (- F) . n is E -measurable by Th37; :: thesis: verum

end;

A10: for x being Element of X st x in E holds
(- F) # x is summable

proof

let x be Element of X; :: thesis: ( x in E implies (- F) # x is summable )
assume x in E ; :: thesis: (- F) # x is summable
then F # x is summable by A5;
hence (- F) # x is summable by Th48; :: thesis: verum

end;

then consider J being ExtREAL_sequence such that
A11: ( ( for n being Nat holds J . n = Integral (M,(((- F) . n) | E)) ) & J is summable & Integral (M,((lim (Partial_Sums (- F))) | E)) = Sum J ) by A6, A7, A3, Th40, A9, MESFUNC9:51;
take I = - J; :: thesis: ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis: ( I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )

proof

let n be Nat; :: thesis: I . n = Integral (M,((F . n) | E))
n in NAT by ORDINAL1:def 12;
then A14: n in dom I by FUNCT_2:def 1;
A12: E c= dom ((- F) . n) by A6, A3, Th40, MESFUNC8:def 2;
(- F) . n = - (F . n) by Th37;
then F . n = - ((- F) . n) by Th36;
then Integral (M,((F . n) | E)) = - (Integral (M,(((- F) . n) | E))) by A12, A9, Th55;
then J . n = - (Integral (M,((F . n) | E))) by A11;
then I . n = - (- (Integral (M,((F . n) | E)))) by A14, MESFUNC1:def 7;
hence I . n = Integral (M,((F . n) | E)) ; :: thesis: verum

end;

thus I is summable by A11, Th45; :: thesis: Integral (M,((lim (Partial_Sums F)) | E)) = Sum I
A15: Partial_Sums J is convergent by A11, MESFUNC9:def 2;
A16: Sum I = lim (Partial_Sums I) by MESFUNC9:def 3
.= lim (- (Partial_Sums J)) by Th44
.= - (lim (Partial_Sums J)) by A15, DBLSEQ_3:17
.= - (Integral (M,((lim (Partial_Sums (- F))) | E))) by A11, MESFUNC9:def 3 ;
deffunc H₁( Nat) -> Element of K19(K20(X,ExtREAL)) = (F . $1) | E;
consider F1 being Functional_Sequence of X,ExtREAL such that
A17: for n being Nat holds F1 . n = H₁(n) from SEQFUNC:sch 1();
reconsider F1 = F1 as with_the_same_dom additive Functional_Sequence of X,ExtREAL by A2, A3, A17, MESFUNC9:18, MESFUNC9:31;
A18: lim (Partial_Sums F1) = (lim (Partial_Sums F)) | E by A1, A2, A3, A17, Th50;
deffunc H₂( Nat) -> Element of K19(K20(X,ExtREAL)) = ((- F) . $1) | E;
consider G1 being Functional_Sequence of X,ExtREAL such that
A19: for n being Nat holds G1 . n = H₂(n) from SEQFUNC:sch 1();
reconsider G1 = G1 as with_the_same_dom additive Functional_Sequence of X,ExtREAL by A7, A8, A19, MESFUNC9:18, MESFUNC9:31;
A20: lim (Partial_Sums G1) = (lim (Partial_Sums (- F))) | E by A6, A7, A19, A3, Th40, Th50;
for n being Element of NAT holds F1 . n = (- G1) . n

proof

let n be Element of NAT ; :: thesis: F1 . n = (- G1) . n
(- F) . n = - (F . n) by Th37;
then A21: (- (- F)) . n = - (- (F . n)) by Th37
.= F . n by DBLSEQ_3:2 ;
A22: F1 . n = (F . n) | E by A17;
(- G1) . n = - (G1 . n) by Th37;
then (- G1) . n = - (((- F) . n) | E) by A19;
then (- G1) . n = (- ((- F) . n)) | E by Th3;
hence F1 . n = (- G1) . n by A21, A22, Th37; :: thesis: verum

end;

then A23: F1 = - G1 by FUNCT_2:def 7;
G1 . 0 = ((- F) . 0) | E by A19;
then A24: dom (G1 . 0) = E by A6, RELAT_1:62;
then A25: for x being Element of X st x in dom (G1 . 0) holds
G1 # x is summable by A6, A10, A19, MESFUNC9:21;
then A26: lim (Partial_Sums F1) = - (lim (Partial_Sums G1)) by A23, Th49;
for n being Nat holds
( G1 . n is E -measurable & G1 . n is without-infty )

proof

let n be Nat; :: thesis: ( G1 . n is E -measurable & G1 . n is without-infty )
thus G1 . n is E -measurable by A6, A9, A19, A3, Th40, MESFUNC9:20; :: thesis: G1 . n is without-infty
((- F) . n) | E is nonnegative by A9, MESFUNC5:15;
hence G1 . n is without-infty by A19; :: thesis: verum

end;

then A27: for n being Nat holds (Partial_Sums G1) . n is E -measurable by MESFUNC9:41;
dom (lim (Partial_Sums G1)) = dom ((Partial_Sums G1) . 0) by MESFUNC8:def 9
.= dom (G1 . 0) by MESFUNC9:def 4 ;
then Integral (M,((- (lim (Partial_Sums G1))) | E)) = - (Integral (M,((lim (Partial_Sums G1)) | E))) by A24, A25, A27, Th55, MESFUNC9:44;
hence Integral (M,((lim (Partial_Sums F)) | E)) = Sum I by A16, A18, A20, A26; :: thesis: verum