let F be FinSequence of ExtREAL ; :: thesis: ( ( for i being Nat st i in dom F holds
F . i <> -infty ) implies Sum F <> -infty )
assume A1: for i being Nat st i in dom F holds
F . i <> -infty ; :: thesis: Sum F <> -infty
consider f being Function of NAT,ExtREAL such that
A2: ( Sum F = f . (len F) & f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 <> -infty );
A4: S₁[ 0 ] by A2;
A5: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A6: S₁[j] ; :: thesis: S₁[j + 1]

now :: thesis: ( j + 1 <= len F implies f . (j + 1) <> -infty )

assume B2: j + 1 <= len F ; :: thesis: f . (j + 1) <> -infty
then A8: f . (j + 1) = (f . j) + (F . (j + 1)) by A2, NAT_1:13;
1 <= j + 1 by NAT_1:11;
then F . (j + 1) <> -infty by A1, B2, FINSEQ_3:25;
hence f . (j + 1) <> -infty by A8, A6, B2, NAT_1:13, XXREAL_3:17; :: thesis: verum

end;

hence S₁[j + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A4, A5);
hence Sum F <> -infty by A2; :: thesis: verum