theorem Th28: :: RFINSEQ2:30

for f being real-valued FinSequence holds
( dom (sort_d f) = dom f & len (sort_d f) = len f )