theorem :: TOPRNS_1:18

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