theorem :: LIOUVIL1:14

for f being Real_Sequence st ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 holds
ex n being Nat st
for k being Nat st k >= n holds
(Partial_Sums f) . k = (Partial_Sums f) . n