( dom f = X & x in X ) by PARTFUN1:def 2;
hence f . x is _Graph by GLIB_000:def 53; :: thesis: verum