let f be real-valued FinSequence; :: thesis: ( dom (sort_a f) = dom f & len (sort_a f) = len f )
f, sort_a f are_fiberwise_equipotent by Def6;
hence ( dom (sort_a f) = dom f & len (sort_a f) = len f ) by RFINSEQ:3; :: thesis: verum