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