let rseq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 implies for n being Element of NAT holds rseq . n = 0 )
assume that
A1: for n being Element of NAT holds 0 <= rseq . n and
A2: rseq is summable and
A3: Sum rseq = 0 ; :: thesis: for n being Element of NAT holds rseq . n = 0
A4: Partial_Sums rseq is bounded_above by A1, A2, SERIES_1:17;
A5: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq

proof

let n be Nat; :: thesis: (Partial_Sums rseq) . n <= Sum rseq
n in NAT by ORDINAL1:def 12;
then (Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A4, SEQ_4:37, SERIES_1:16;
hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

end;

A6: Partial_Sums rseq is V45() by A1, SERIES_1:16;

now

given n1 being Element of NAT such that A7: rseq . n1 <> 0 ; :: thesis: contradiction
A8: for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (Partial_Sums rseq) . n
A9: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def 1;
0 <= rseq . 0 by A1;
hence 0 <= (Partial_Sums rseq) . n by A6, A9, SEQM_3:5; :: thesis: verum

end;

(Partial_Sums rseq) . n1 > 0

proof

now

per cases ( n1 = 0 or n1 <> 0 ) ;

case A10: n1 = 0 ; :: thesis: (Partial_Sums rseq) . n1 > 0

then (Partial_Sums rseq) . n1 = rseq . 0 by SERIES_1:def 1;
hence (Partial_Sums rseq) . n1 > 0 by A1, A7, A10; :: thesis: verum

end;

case A11: n1 <> 0 ; :: thesis: (Partial_Sums rseq) . n1 > 0

set nn = n1 - 1;
A12: ( (n1 - 1) + 1 = n1 & 0 <= rseq . n1 ) by A1;
0 <= n1 by NAT_1:2;
then 0 + 1 <= n1 by A11, INT_1:7;
then A13: n1 - 1 in NAT by INT_1:5;
then 0 <= (Partial_Sums rseq) . (n1 - 1) by A8;
then (rseq . n1) + 0 <= (rseq . n1) + ((Partial_Sums rseq) . (n1 - 1)) by XREAL_1:7;
hence (Partial_Sums rseq) . n1 > 0 by A7, A13, A12, SERIES_1:def 1; :: thesis: verum

end;

end;

end;

hence (Partial_Sums rseq) . n1 > 0 ; :: thesis: verum

end;

hence contradiction by A3, A5; :: thesis: verum

end;

hence for n being Element of NAT holds rseq . n = 0 ; :: thesis: verum