theorem Th30: :: BASEL_2:30

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