let F be FinSequence of ExtREAL ; :: thesis: ( ( for n being Nat st n in dom F holds
0 <= F . n ) implies 0 <= Sum F )
assume A1: for n being Nat st n in dom F holds
0 <= F . n ; :: thesis: 0 <= Sum F
consider sumf being Function of NAT ,ExtREAL such that
A2: ( Sum F = sumf . (len F) & sumf . 0 = 0 & ( for n being Element of NAT st n < len F holds
sumf . (n + 1) = (sumf . n) + (F . (n + 1)) ) ) by CONVFUN1:def 5;
defpred S₁[ Nat] means ( $1 <= len F implies 0 <= sumf . $1 );
A3: S₁[ 0 ] by A2;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

end;

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