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 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 ) ) 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL 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 ) ) 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL 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 ) ) 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: for F being Functional_Sequence of X,ExtREAL 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 ) ) 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: ( 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 ) ) 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_measurable_on E & F . n is nonnegative ) ; :: 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 PF = Partial_Sums F;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
A5: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
take I ; :: thesis: for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
A6: for n being Nat holds F . n is without-infty by A4, MESFUNC5:18;
thus for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n ) :: thesis: verum

proof

set PI = Partial_Sums I;
defpred S₁[ Nat] means Integral M,((Partial_Sums F) . $1) = (Partial_Sums I) . $1;
let n be Nat; :: thesis: ( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
reconsider n9 = n as Element of NAT by ORDINAL1:def 13;
I . n = Integral M,(F . n9) by A5;
hence I . n = Integral M,(F . n) ; :: thesis: Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
A9: F . (k + 1) is_measurable_on E by A4;
A10: dom (F . (k + 1)) = E by A1, A3, MESFUNC8:def 2;
A11: (Partial_Sums F) . (k + 1) is_measurable_on E by A4, A6, Th41;
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, A6, 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, A10, A9, A13, A12, MESFUNC5:84;
A18: D = (dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1))) by A13, A12, A16, MESFUNC5:28
.= E by A14, A10 ;
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 A10, 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 A4, A11, Th36, 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 A10, A9, A12, A20, MESFUNC5:94
.= ((Partial_Sums I) . k) + (I . (k + 1)) by A5, A8 ;
hence S₁[k + 1] by Def1; :: thesis: verum
reconsider k1 = k + 1 as Nat ;

end;

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

end;