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_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A2;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A9, A5);

hence 0 <= Sum F by A1; :: thesis: verum

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

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

S

proof

A9:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A6: S_{1}[n]
; :: thesis: S_{1}[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;assume A6: S

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

for n being Nat holds S

hence 0 <= Sum F by A1; :: thesis: verum