theorem :: RFINSEQ2:21

for f being real-valued non-decreasing FinSequence holds sort_a f = f