let n be Nat; :: thesis: ( n >= 1 implies dseq . n <= Sum eseq )
assume A1: n >= 1 ; :: thesis: dseq . n <= Sum eseq
then for k being Nat holds
( 0 <= (cseq n) . k & (cseq n) . k <= eseq . k ) by Th14;
then Sum (cseq n) <= Sum eseq by Th23, SERIES_1:20;
hence dseq . n <= Sum eseq by A1, Th21; :: thesis: verum