for X being RealNormSpace
for s being sequence of X st s is summable holds
for n being Nat holds s ^\ n is summable