for f being INT -valued Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
Sum f is Integer