for seq1, seq2 being Real_Sequence holds
( seq1 = - seq2 iff for n being Nat holds seq1 . n = - (seq2 . n) )