A3: dom f c= X by RELAT_1:def 18;
A4: rng (Im f) c= REAL by VALUED_0:def 3;
dom (Im f) = dom f by Def4;
hence Im f is PartFunc of X,REAL by A3, A4, RELSET_1:4; :: thesis: verum