for n being Nat holds (Partial_Sums Reci-seq1) . n < - 2