let f be real-valued FinSequence; :: thesis: sort_d (- f) = - (sort_a f)
- f, sort_d (- f) are_fiberwise_equipotent by Def5;
then A1: - (- f), - (sort_d (- f)) are_fiberwise_equipotent by Th25;
- (sort_d (- f)) is non-decreasing by Th22;
then - (sort_d (- f)) = sort_a f by A1, Def6;
hence sort_d (- f) = - (sort_a f) ; :: thesis: verum