rng f = rng (sort_a f) by CLASSES1:75, RFINSEQ2:def 6;
hence sort_a f is natural-valued by VALUED_0:def 6, RELAT_1:def 19; :: thesis: verum