for X being RealUnitarySpace
for seq being sequence of X st ex k being Nat st seq ^\ k is summable holds
seq is summable