for f being Real_Sequence st f is absolutely_summable holds
|.(Sum f).| <= Sum (abs f)