theorem :: RSSPACE:17

for rseq being Real_Sequence st ( for n being Nat holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 holds
for n being Nat holds rseq . n = 0