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