theorem :: RFINSEQ2:29

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