for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.| by Lm6;