for rseq1 being Real_Sequence
for seq2 being Complex_Sequence st rseq1 is summable & ex m being Nat st
for n being Nat st m <= n holds
|.(seq2 . n).| <= rseq1 . n holds
seq2 is absolutely_summable