theorem :: SEQ_1:29

for seq1, seq2 being Real_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;