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