for seq being Real_Sequence st seq ^\ 1 is summable holds
( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) )