for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1 ;