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 E -measurable & 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 E -measurable & 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 E -measurable & 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 E -measurable & 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 E -measurable & 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 E -measurable & 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 sequence of 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:12;
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 12;
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 E -measurable by A4;
A10: dom (F . (k + 1)) = E by A1, A3;
A11: (Partial_Sums F) . (k + 1) is E -measurable 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 E -measurable 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:78;
A18: D = (dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1))) by A13, A12, A16, MESFUNC5:22
.= E by A14, A10 ;
then A19: ((Partial_Sums F) . k) | D = (Partial_Sums F) . k by A14;
A20: (F . (k + 1)) | D = F . (k + 1) by A10, 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 A4, A11, Th36, 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 A10, A9, A12, A20, MESFUNC5:88
.= ((Partial_Sums I) . k) + (I . (k + 1)) by A5, A8 ;
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 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;