let X be non empty set ; :: thesis: for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_-infty-valued
let F be without_-infty-valued FinSequence of Funcs (X,ExtREAL); :: thesis: Partial_Sums F is without_-infty-valued
defpred S₁[ Nat] means ( $1 in dom (Partial_Sums F) implies (Partial_Sums F) . $1 is without-infty );
A1: S₁[ 0 ] by FINSEQ_3:24;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
B4: len F = len (Partial_Sums F) by DEF13;
then A4: dom F = dom (Partial_Sums F) by FINSEQ_3:29;
assume A5: n + 1 in dom (Partial_Sums F) ; :: thesis: (Partial_Sums F) . (n + 1) is without-infty

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

suppose A6: n = 0 ; :: thesis: (Partial_Sums F) . (n + 1) is without-infty

then F . 1 is without-infty by A4, A5, DEF11;
hence (Partial_Sums F) . (n + 1) is without-infty by A6, DEF13; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (Partial_Sums F) . (n + 1) is without-infty

then A8: n >= 1 by NAT_1:14;
A7: n + 1 <= len F by A5, B4, FINSEQ_3:25;
then A9: n < len F by NAT_1:13;
F . (n + 1) is without-infty by A4, A5, DEF11;
then reconsider p = (Partial_Sums F) /. n, q = F /. (n + 1) as without-infty Function of X,ExtREAL by A9, A3, A4, A5, A8, FINSEQ_3:25, PARTFUN1:def 6;
p + q is without-infty Function of X,ExtREAL ;
hence (Partial_Sums F) . (n + 1) is without-infty by A8, A7, DEF13, NAT_1:13; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence Partial_Sums F is without_-infty-valued ; :: thesis: verum