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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & 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:18;
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_measurable_on E by A4;
A9: dom (F . (k + 1)) = E by A1, A3, MESFUNC8:def 2;
A10: (Partial_Sums F) . (k + 1) is_measurable_on E 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_measurable_on E 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:84;
A18: D = E /\ E by A14, A9, A13, A12, A16, MESFUNC5:28;
then A19: ((Partial_Sums F) . k) | D = (Partial_Sums F) . k by A14, RELAT_1:97;
A20: (F . (k + 1)) | D = F . (k + 1) by A9, A18, RELAT_1:97;
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:94
.= (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:94
.= (Integral M,((Partial_Sums F) . k)) + (Integral M,(F . (k + 1))) by A9, A8, A12, A20, MESFUNC5:94
.= ((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;