theorem Th7: :: COMSEQ_1:7

for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)