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