let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
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 nonnegative & 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL
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 nonnegative & 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL
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 nonnegative & 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 F being Functional_Sequence of X,ExtREAL
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 nonnegative & 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 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 nonnegative & 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 nonnegative & 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 nonnegative & 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 nonnegative & I . n = Integral (M,(F . n)) ) ; :: thesis: Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m
set PF = Partial_Sums F;
A5: for n being Nat holds F . n is without-infty by A4, MESFUNC5:12;
thus Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m :: thesis: verum

proof

set PI = Partial_Sums I;
defpred S₁[ Nat] means Integral (M,((Partial_Sums F) . $1)) = (Partial_Sums I) . $1;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: F . (k + 1) is E -measurable by A4;
A9: dom (F . (k + 1)) = E by A1, A3;
A10: (Partial_Sums F) . (k + 1) is E -measurable by A4, A5, Th41;
A11: (Partial_Sums F) . (k + 1) is nonnegative by A4, Th36;
A12: F . (k + 1) is nonnegative by A4;
A13: (Partial_Sums F) . k is nonnegative by A4, Th36;
A14: dom ((Partial_Sums F) . k) = E by A1, A2, A3, Th29;
A15: (Partial_Sums F) . k is E -measurable by A4, A5, Th41;
then consider D being Element of S such that
A16: D = dom (((Partial_Sums F) . k) + (F . (k + 1))) and
A17: integral+ (M,(((Partial_Sums F) . k) + (F . (k + 1)))) = (integral+ (M,(((Partial_Sums F) . k) | D))) + (integral+ (M,((F . (k + 1)) | D))) by A14, A9, A8, A13, A12, MESFUNC5:78;
A18: D = E /\ E by A14, A9, A13, A12, A16, MESFUNC5:22;
then A19: ((Partial_Sums F) . k) | D = (Partial_Sums F) . k by A14;
A20: (F . (k + 1)) | D = F . (k + 1) by A9, A18;
dom ((Partial_Sums F) . (k + 1)) = E by A1, A2, A3, Th29;
then Integral (M,((Partial_Sums F) . (k + 1))) = integral+ (M,((Partial_Sums F) . (k + 1))) by A10, A11, MESFUNC5:88
.= (integral+ (M,(((Partial_Sums F) . k) | D))) + (integral+ (M,((F . (k + 1)) | D))) by A17, Def4
.= (Integral (M,((Partial_Sums F) . k))) + (integral+ (M,((F . (k + 1)) | D))) by A14, A15, A13, A19, MESFUNC5:88
.= (Integral (M,((Partial_Sums F) . k))) + (Integral (M,(F . (k + 1)))) by A9, A8, A12, A20, MESFUNC5:88
.= ((Partial_Sums I) . k) + (I . (k + 1)) by A4, A7 ;
hence S₁[k + 1] by Def1; :: thesis: verum

end;

Integral (M,((Partial_Sums F) . 0)) = Integral (M,(F . 0)) by Def4;
then Integral (M,((Partial_Sums F) . 0)) = I . 0 by A4;
then A21: S₁[ 0 ] by Def1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A6);
hence Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m ; :: thesis: verum

end;