rng f = rng (sort_d f) by CLASSES1:75, RFINSEQ2:def 5;
hence sort_d f is integer-valued by VALUED_0:def 5, RELAT_1:def 19; :: thesis: verum