theorem :: RFINSEQ2:21

for f being non-decreasing FinSequence of REAL holds sort_a f = f by Def6;