theorem :: RFINSEQ2:20

for f being real-valued non-increasing FinSequence holds sort_d f = f