rng f = rng (Rev f) by Th60;
hence Rev f is XFinSequence of D by ORDINAL1:def 8; :: thesis: verum