theorem Th22: :: LOPBAN_3:22
for X being RealNormSpace
for s being sequence of X st s is summable holds
for n being Nat holds s ^\ n is summable