theorem :: RFINSEQ2:20

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