theorem Th12: :: LIOUVIL1:10

for f being Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
f is summable