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