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