theorem Th13: :: SEQ_1:13

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