for f being non-increasing FinSequence of REAL holds sort_d f = f by Def5;