for X being RealBanachSpace
for s being sequence of X st s is norm_summable holds
||.(Sum s).|| <= Sum ||.s.||