theorem :: SEQ_1:11

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