theorem :: MOEBIUS3:28

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