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 = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

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 = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) implies ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n ) )

assume that

A1: E = 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 E -measurable & F . n is nonpositive ) ; :: thesis: ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

set G = - F;

(- F) . 0 = - (F . 0) by Th37;

then A5: E = dom ((- F) . 0) by A1, MESFUNC1:def 7;

A7: - F is with_the_same_dom by A3, Th40;

for n being Nat holds

( (- F) . n is E -measurable & (- F) . n is nonnegative )

A8: for n being Nat holds

( J . n = Integral (M,((- F) . n)) & Integral (M,((Partial_Sums (- F)) . n)) = (Partial_Sums J) . n ) by A5, A7, A2, Th41, MESFUNC9:50;

set I = - J;

take - J ; :: thesis: for n being Nat holds

( (- J) . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n )

A10: for n being Nat holds

( F . n is E -measurable & F . n is V121() )

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

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 = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is E -measurable & F . n is nonpositive ) ) implies ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n ) )

assume that

A1: E = 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 E -measurable & F . n is nonpositive ) ; :: thesis: ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

set G = - F;

(- F) . 0 = - (F . 0) by Th37;

then A5: E = dom ((- F) . 0) by A1, MESFUNC1:def 7;

A7: - F is with_the_same_dom by A3, Th40;

for n being Nat holds

( (- F) . n is E -measurable & (- F) . n is nonnegative )

proof

then consider J being ExtREAL_sequence such that
let n be Nat; :: thesis: ( (- F) . n is E -measurable & (- F) . n is nonnegative )

( E = dom (F . n) & F . n is E -measurable ) by A4, A1, A3, MESFUNC8:def 2;

then - (F . n) is E -measurable by MEASUR11:63;

hence (- F) . n is E -measurable by Th37; :: thesis: (- F) . n is nonnegative

F . n is nonpositive by A4;

then - (F . n) is nonnegative ;

hence (- F) . n is nonnegative by Th37; :: thesis: verum

end;( E = dom (F . n) & F . n is E -measurable ) by A4, A1, A3, MESFUNC8:def 2;

then - (F . n) is E -measurable by MEASUR11:63;

hence (- F) . n is E -measurable by Th37; :: thesis: (- F) . n is nonnegative

F . n is nonpositive by A4;

then - (F . n) is nonnegative ;

hence (- F) . n is nonnegative by Th37; :: thesis: verum

A8: for n being Nat holds

( J . n = Integral (M,((- F) . n)) & Integral (M,((Partial_Sums (- F)) . n)) = (Partial_Sums J) . n ) by A5, A7, A2, Th41, MESFUNC9:50;

set I = - J;

take - J ; :: thesis: for n being Nat holds

( (- J) . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n )

A10: for n being Nat holds

( F . n is E -measurable & F . n is V121() )

proof

let n be Nat; :: thesis: ( F . n is E -measurable & F . n is V121() )

thus F . n is E -measurable by A4; :: thesis: F . n is V121()

F . n is nonpositive by A4;

hence F . n is V121() ; :: thesis: verum

end;thus F . n is E -measurable by A4; :: thesis: F . n is V121()

F . n is nonpositive by A4;

hence F . n is V121() ; :: thesis: verum

hereby :: thesis: verum

let n be Nat; :: thesis: ( (- J) . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n )

dom (- J) = NAT by FUNCT_2:def 1;

then n in dom (- J) by ORDINAL1:def 12;

then (- J) . n = - (J . n) by MESFUNC1:def 7;

then A9: (- J) . n = - (Integral (M,((- F) . n))) by A8;

( E = dom (F . n) & F . n is E -measurable & (- F) . n = - (F . n) ) by A4, A1, A3, Th37, MESFUNC8:def 2;

then Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by Th52;

hence (- J) . n = Integral (M,(F . n)) by A9; :: thesis: Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n

A11: E = dom ((Partial_Sums F) . n) by A1, A2, A3, MESFUNC9:29;

(Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n by Th42

.= - ((Partial_Sums F) . n) by Th37 ;

then A13: Integral (M,((Partial_Sums (- F)) . n)) = - (Integral (M,((Partial_Sums F) . n))) by A10, A1, A3, A11, Th52, Th67;

(Partial_Sums (- J)) . n = - ((Partial_Sums J) . n) by Th43

.= - (Integral (M,((Partial_Sums (- F)) . n))) by A8 ;

hence Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n by A13; :: thesis: verum

end;dom (- J) = NAT by FUNCT_2:def 1;

then n in dom (- J) by ORDINAL1:def 12;

then (- J) . n = - (J . n) by MESFUNC1:def 7;

then A9: (- J) . n = - (Integral (M,((- F) . n))) by A8;

( E = dom (F . n) & F . n is E -measurable & (- F) . n = - (F . n) ) by A4, A1, A3, Th37, MESFUNC8:def 2;

then Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by Th52;

hence (- J) . n = Integral (M,(F . n)) by A9; :: thesis: Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n

A11: E = dom ((Partial_Sums F) . n) by A1, A2, A3, MESFUNC9:29;

(Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n by Th42

.= - ((Partial_Sums F) . n) by Th37 ;

then A13: Integral (M,((Partial_Sums (- F)) . n)) = - (Integral (M,((Partial_Sums F) . n))) by A10, A1, A3, A11, Th52, Th67;

(Partial_Sums (- J)) . n = - ((Partial_Sums J) . n) by Th43

.= - (Integral (M,((Partial_Sums (- F)) . n))) by A8 ;

hence Integral (M,((Partial_Sums F) . n)) = (Partial_Sums (- J)) . n by A13; :: thesis: verum