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