let F be FinSequence of ExtREAL ; :: thesis: ( ( for n being Nat st n in dom F holds
0 <= F . n ) implies 0 <= Sum F )
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: 0 <= Sum F
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
assume A7: n + 1 <= len F ; :: thesis: 0 <= sumf . (n + 1)
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: verum

end;

A9: S₁[ 0 ] by A2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A5);
hence 0 <= Sum F by A1; :: thesis: verum