let F be FinSequence of ExtREAL ; :: thesis:
consider sumf being sequence of ExtREAL such that
A1: Sum F = sumf . (len F) and
A2: sumf . 0 = 0 and
A3: for n being Nat st n < len F holds
sumf . (n + 1) = (sumf . n) + (F . (n + 1)) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len F implies 0 <= sumf . $1 );
assume A4: for n being Nat st n in dom F holds
0 <= F . n ; :: thesis:
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A6: S₁[n] ; :: thesis:
assume A7: n + 1 <= len F ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
1 <= n + 1 by NAT_1:11;
then n + 1 in Seg (len F) by A7;
then n + 1 in dom F by FINSEQ_1:def 3;
then A8: 0 <= F . (n + 1) by A4;
n < len F by A7, NAT_1:13;
then sumf . (n + 1) = (sumf . n) + (F . (n + 1)) by A3;
hence 0 <= sumf . (n + 1) by A6, A7, A8, NAT_1:13; :: thesis:

end;