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]
B1: 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, DEF10;
hence (Partial_Sums F) . (n + 1) is without+infty by A6, DEF13; :: thesis: verum

end;

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

then A8: n >= 1 by NAT_1:14;
n + 1 <= len F by A5, B1, FINSEQ_3:25;
then A9: n < len F by NAT_1:13;
F . (n + 1) is without+infty by A4, A5, DEF10;
then reconsider p = (Partial_Sums F) /. n, q = F /. (n + 1) as without+infty Function of X,ExtREAL by A3, A4, A5, A8, A9, 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 A7, A9, DEF13, NAT_1:14; :: 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