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