rng (X --> 0) = {0} by FUNCOP_1:8;
hence {} in rng (X --> 0) by TARSKI:def 1; :: according to RELAT_1:def 9 :: thesis: verum