let X be non empty set ; :: thesis: for S being SigmaField of X
for P being Element of S
for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds
F /. n is P -measurable ) holds
for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable
let S be SigmaField of X; :: thesis: for P being Element of S
for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds
F /. n is P -measurable ) holds
for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable
let P be Element of S; :: thesis: for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds
F /. n is P -measurable ) holds
for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable
let F be summable FinSequence of Funcs (X,ExtREAL); :: thesis: ( ( for n being Nat st n in dom F holds
F /. n is P -measurable ) implies for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable )
assume A1: for n being Nat st n in dom F holds
F /. n is P -measurable ; :: thesis: for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable
A2: P c= X ;
A3: len F = len (Partial_Sums F) by DEF13;
then A4: dom F = dom (Partial_Sums F) by FINSEQ_3:29;
defpred S₁[ Nat] means ( $1 in dom F implies (Partial_Sums F) /. $1 is P -measurable );

per cases ( F is without_+infty-valued or F is without_-infty-valued ) by DEF12;

suppose A5: F is without_+infty-valued ; :: thesis: for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable

A6: S₁[ 0 ] by FINSEQ_3:24;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
assume A9: n + 1 in dom F ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

per cases ( n = 0 or n <> 0 ) ;

suppose A10: n = 0 ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

then (Partial_Sums F) /. (n + 1) = (Partial_Sums F) . 1 by A4, A9, PARTFUN1:def 6
.= F . 1 by DEF13
.= F /. 1 by A9, A10, PARTFUN1:def 6 ;
hence (Partial_Sums F) /. (n + 1) is P -measurable by A1, A9, A10; :: thesis: verum

end;

suppose A11: n <> 0 ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

then A12: n >= 1 by NAT_1:14;
n + 1 <= len F by A9, FINSEQ_3:25;
then A13: n < len F by NAT_1:13;
then A15: ( F /. (n + 1) = F . (n + 1) & (Partial_Sums F) /. n = (Partial_Sums F) . n & (Partial_Sums F) /. (n + 1) = (Partial_Sums F) . (n + 1) ) by A4, A9, A12, FINSEQ_3:25, PARTFUN1:def 6;
then A16: (Partial_Sums F) /. (n + 1) = ((Partial_Sums F) /. n) + (F /. (n + 1)) by A11, A13, NAT_1:14, DEF13;
Partial_Sums F is without_+infty-valued by A5, Th56;
then A17: ( F /. (n + 1) is without+infty & (Partial_Sums F) /. n is without+infty ) by A5, A9, A12, A15, A13, A3, FINSEQ_3:25;
then A19: dom (((Partial_Sums F) /. n) + (F /. (n + 1))) = (dom ((Partial_Sums F) /. n)) /\ (dom (F /. (n + 1))) by MESFUNC9:1;
A18: ( P c= dom ((Partial_Sums F) /. n) & P c= dom (F /. (n + 1)) ) by A2, FUNCT_2:def 1;
F /. (n + 1) is P -measurable by A9, A1;
hence (Partial_Sums F) /. (n + 1) is P -measurable by A8, A12, A13, A16, A17, A18, A19, Th61, FINSEQ_3:25, XBOOLE_1:19; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
hence for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable ; :: thesis: verum

end;

suppose A19: F is without_-infty-valued ; :: thesis: for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable

A20: S₁[ 0 ] by FINSEQ_3:24;
A21: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A24: S₁[n] ; :: thesis: S₁[n + 1]
assume A25: n + 1 in dom F ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

per cases ( n = 0 or n <> 0 ) ;

suppose A26: n = 0 ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

then (Partial_Sums F) /. (n + 1) = (Partial_Sums F) . 1 by A25, A4, PARTFUN1:def 6
.= F . 1 by DEF13
.= F /. 1 by A25, A26, PARTFUN1:def 6 ;
hence (Partial_Sums F) /. (n + 1) is P -measurable by A1, A25, A26; :: thesis: verum

end;

suppose A27: n <> 0 ; :: thesis: (Partial_Sums F) /. (n + 1) is P -measurable

then A28: n >= 1 by NAT_1:14;
n + 1 <= len F by A25, FINSEQ_3:25;
then A29: n < len F by NAT_1:13;
then A30: ( F /. (n + 1) = F . (n + 1) & (Partial_Sums F) /. n = (Partial_Sums F) . n & (Partial_Sums F) /. (n + 1) = (Partial_Sums F) . (n + 1) ) by A4, A25, A28, FINSEQ_3:25, PARTFUN1:def 6;
then A31: (Partial_Sums F) /. (n + 1) = ((Partial_Sums F) /. n) + (F /. (n + 1)) by A27, A29, DEF13, NAT_1:14;
Partial_Sums F is without_-infty-valued by A19, Th57;
then A32: ( F /. (n + 1) is without-infty & (Partial_Sums F) /. n is without-infty ) by A19, A25, A29, A3, A28, A30, FINSEQ_3:25;
F /. (n + 1) is P -measurable by A25, A1;
hence (Partial_Sums F) /. (n + 1) is P -measurable by A31, A32, A29, A24, A28, FINSEQ_3:25, MESFUNC5:31; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A21);
hence for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable ; :: thesis: verum

end;

end;