rng (rf - X) c= rng rf by FINSEQ_3:66;
then rng (rf - X) c= REAL by XBOOLE_1:1;
hence rf - X is real-valued by VALUED_0:def 3; :: thesis: verum