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

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

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

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

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

for E being Element of S

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let E be Element of S; :: thesis: for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let I be ExtREAL_sequence; :: thesis: for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let m be Nat; :: 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 & I . n = Integral (M,(F . n)) ) ) implies Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m )

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 & I . n = Integral (M,(F . n)) ) ; :: thesis: Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

set G = - F;

set J = - I;

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

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

A6: - F is with_the_same_dom by A3, Th40;

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

A8: for n being Nat holds

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

( (- F) . n is E -measurable & (- F) . n is nonnegative & (- I) . n = Integral (M,((- F) . n)) )

then Integral (M,((- (Partial_Sums F)) . m)) = (Partial_Sums (- I)) . m by Th42;

then Integral (M,((- (Partial_Sums F)) . m)) = - ((Partial_Sums I) . m) by Th43;

then Integral (M,(- ((Partial_Sums F) . m))) = - ((Partial_Sums I) . m) by Th37;

then - (Integral (M,((Partial_Sums F) . m))) = - ((Partial_Sums I) . m) by A1, A3, A7, A8, Th67, Th52;

hence Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m by XXREAL_3:10; :: thesis: verum

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

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

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

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

for E being Element of S

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S

for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let E be Element of S; :: thesis: for I being ExtREAL_sequence

for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let I be ExtREAL_sequence; :: thesis: for m being Nat 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 & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

let m be Nat; :: 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 & I . n = Integral (M,(F . n)) ) ) implies Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m )

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 & I . n = Integral (M,(F . n)) ) ; :: thesis: Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

set G = - F;

set J = - I;

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

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

A6: - F is with_the_same_dom by A3, Th40;

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

A8: for n being Nat holds

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

proof

for n being Nat holds
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

( (- F) . n is E -measurable & (- F) . n is nonnegative & (- I) . n = Integral (M,((- F) . n)) )

proof

then
Integral (M,((Partial_Sums (- F)) . m)) = (Partial_Sums (- I)) . m
by A5, A2, A6, Th41, MESFUNC9:46;
let n be Nat; :: thesis: ( (- F) . n is E -measurable & (- F) . n is nonnegative & (- I) . n = Integral (M,((- F) . n)) )

A9: ( F . n is nonpositive & I . n = Integral (M,(F . n)) ) by A4;

A10: (- F) . n = - (F . n) by Th37;

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

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

A12: dom (F . n) = E by A1, A3, MESFUNC8:def 2;

hence (- F) . n is E -measurable by A4, A10, MEASUR11:63; :: thesis: ( (- F) . n is nonnegative & (- I) . n = Integral (M,((- F) . n)) )

thus (- F) . n is nonnegative by A9, A10; :: thesis: (- I) . n = Integral (M,((- F) . n))

Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by A4, A10, A12, Th52;

hence (- I) . n = Integral (M,((- F) . n)) by A9, A11, MESFUNC1:def 7; :: thesis: verum

end;A9: ( F . n is nonpositive & I . n = Integral (M,(F . n)) ) by A4;

A10: (- F) . n = - (F . n) by Th37;

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

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

A12: dom (F . n) = E by A1, A3, MESFUNC8:def 2;

hence (- F) . n is E -measurable by A4, A10, MEASUR11:63; :: thesis: ( (- F) . n is nonnegative & (- I) . n = Integral (M,((- F) . n)) )

thus (- F) . n is nonnegative by A9, A10; :: thesis: (- I) . n = Integral (M,((- F) . n))

Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by A4, A10, A12, Th52;

hence (- I) . n = Integral (M,((- F) . n)) by A9, A11, MESFUNC1:def 7; :: thesis: verum

then Integral (M,((- (Partial_Sums F)) . m)) = (Partial_Sums (- I)) . m by Th42;

then Integral (M,((- (Partial_Sums F)) . m)) = - ((Partial_Sums I) . m) by Th43;

then Integral (M,(- ((Partial_Sums F) . m))) = - ((Partial_Sums I) . m) by Th37;

then - (Integral (M,((Partial_Sums F) . m))) = - ((Partial_Sums I) . m) by A1, A3, A7, A8, Th67, Th52;

hence Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m by XXREAL_3:10; :: thesis: verum