for n being Nat holds (Partial_Sums Basel-seq) . n >= 0