for m being Nat holds Basel-seq1 . m <= Sum (Basel-seq,m)