a1: dom f c= X by RELAT_1:def 18;
a2: rng (Im f) c= REAL by VALUED_0:def 3;
dom (Im f) = dom f by Def2a;
hence Im f is PartFunc of X,REAL by a1, a2, RELSET_1:11; :: thesis: verum