theorem :: SEQ_1:30
for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3