let f be FinSequence of REAL ; :: 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:16; :: thesis: verum