theorem :: RFINSEQ2:28

for f being FinSequence of REAL holds sort_d (- f) = - (sort_a f)