rng f = rng (Rev f) by Th60;
then rng (Rev f) c= D by RELAT_1:def 19;
hence Rev f is XFinSequence of by RELAT_1:def 19; :: thesis: verum