rng (x .--> i) = {i} by RELAT_1:160;
hence rng (x .--> i) c= A by ZFMISC_1:31; :: according to RELAT_1:def 19 :: thesis: verum