theorem :: TOPRNS_1:20

for N being Nat
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th10;