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 Def3;
hence Re f is PartFunc of X,REAL by A1, A2, RELSET_1:4; :: thesis: verum