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) )