theorem Th54: :: COMSEQ_3:54

for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )