theorem :: RFINSEQ2:28

for f being real-valued FinSequence holds sort_d (- f) = - (sort_a f)