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 )

(- F) # x is summable

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 )

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_{1}( 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_{1}(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_{2}( 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_{2}(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

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 V120() )

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

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

A10:
for x being Element of X st x in E holds
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;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

(- F) # x is summable

proof

then consider J being ExtREAL_sequence such that
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;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

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

thus
I is summable
by A11, Th45; :: thesis: Integral (M,((lim (Partial_Sums F)) | E)) = Sum I
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;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

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

consider F1 being Functional_Sequence of X,ExtREAL such that

A17: for n being Nat holds F1 . n = H

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

consider G1 being Functional_Sequence of X,ExtREAL such that

A19: for n being Nat holds G1 . n = H

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

then A23:
F1 = - G1
by FUNCT_2:def 7;
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;(- 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

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 V120() )

proof

then A27:
for n being Nat holds (Partial_Sums G1) . n is E -measurable
by MESFUNC9:41;
let n be Nat; :: thesis: ( G1 . n is E -measurable & G1 . n is V120() )

thus G1 . n is E -measurable by A6, A9, A19, A3, Th40, MESFUNC9:20; :: thesis: G1 . n is V120()

((- F) . n) | E is nonnegative by A9, MESFUNC5:15;

hence G1 . n is V120() by A19; :: thesis: verum

end;thus G1 . n is E -measurable by A6, A9, A19, A3, Th40, MESFUNC9:20; :: thesis: G1 . n is V120()

((- F) . n) | E is nonnegative by A9, MESFUNC5:15;

hence G1 . n is V120() by A19; :: thesis: verum

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