for n being Nat st n >= 1 holds
dseq . n <= Sum eseq