for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds
( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )