theorem Th29: :: RFINSEQ2:31

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