let f be real-valued non-increasing FinSequence; :: thesis: sort_d f = f
f is FinSequence of REAL by RVSUM_1:145;
hence sort_d f = f by Def5; :: thesis: verum