for n being Nat holds (Partial_Sums Basel-seq) . n < 5 / 3