for seq being ExtREAL_sequence st seq is summable holds
- seq is summable