:: deftheorem defines - TOPRNS_1:def 5 :
for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 - seq2 = seq1 + (- seq2);