rng (Rev f) = rng f by FINSEQ_5:57;
then rng (Rev f) c= D by RELAT_1:def 19;
hence Rev f is D -valued by RELAT_1:def 19; :: thesis: verum