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 ()) | 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 ()) | 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 ()) | 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 ()) | 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 ()) | E)) = Sum I ) )

assume that
A1: E c= dom (F . 0) 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 ()) | E)) = Sum I )

set G = - F;
(- F) . 0 = - (F . 0) by Th37;
then A6: E c= dom ((- F) . 0) by ;
A7: - F is additive by ;
A8: - F is with_the_same_dom by ;
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 ;
then - (F . n) is E -measurable by ;
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 ;
take I = - J; :: thesis: ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim ()) | E)) = Sum I )
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis: ( I is summable & Integral (M,((lim ()) | 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 ;
(- 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 ;
then J . n = - (Integral (M,((F . n) | E))) by A11;
then I . n = - (- (Integral (M,((F . n) | E)))) by ;
hence I . n = Integral (M,((F . n) | E)) ; :: thesis: verum
end;
thus I is summable by ; :: thesis: Integral (M,((lim ()) | E)) = Sum I
A15: Partial_Sums J is convergent by ;
A16: Sum I = lim () by MESFUNC9:def 3
.= lim (- ()) by Th44
.= - (lim ()) by
.= - (Integral (M,((lim (Partial_Sums (- F))) | E))) by ;
deffunc H1( 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 = H1(n) from reconsider F1 = F1 as with_the_same_dom additive Functional_Sequence of X,ExtREAL by ;
A18: lim () = (lim ()) | E by A1, A2, A3, A17, Th50;
deffunc H2( 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 = H2(n) from reconsider G1 = G1 as with_the_same_dom additive Functional_Sequence of X,ExtREAL by ;
A20: lim () = (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 ; :: 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 ;
then A25: for x being Element of X st x in dom (G1 . 0) holds
G1 # x is summable by ;
then A26: lim () = - (lim ()) by ;
for n being Nat holds
( G1 . n is E -measurable & G1 . n is V120() )
proof
let n be Nat; :: thesis: ( G1 . n is E -measurable & G1 . n is V120() )
thus G1 . n is E -measurable by ; :: thesis: G1 . n is V120()
((- F) . n) | E is nonnegative by ;
hence G1 . n is V120() by A19; :: thesis: verum
end;
then A27: for n being Nat holds () . n is E -measurable by MESFUNC9:41;
dom (lim ()) = dom (() . 0) by MESFUNC8:def 9
.= dom (G1 . 0) by MESFUNC9:def 4 ;
then Integral (M,((- (lim ())) | E)) = - (Integral (M,((lim ()) | E))) by ;
hence Integral (M,((lim ()) | E)) = Sum I by A16, A18, A20, A26; :: thesis: verum