theorem LM0: :: LOPBAN13:2

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