let n be Element of NAT ; :: thesis: ( n >= 1 implies dseq . n <= Sum eseq )
assume A1: n >= 1 ; :: thesis: dseq . n <= Sum eseq
then for k being Element of NAT holds
( 0 <= (cseq n) . k & (cseq n) . k <= eseq . k ) by Th15;
then Sum (cseq n) <= Sum eseq by Th24, SERIES_1:20;
hence dseq . n <= Sum eseq by A1, Th22; :: thesis: verum