for seq1, seq2 being Complex_Sequence st ( for n being Nat holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable holds
( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) by SERIES_1:20;