dom f = X by PARTFUN1:def 2;
hence f . x is Category by Def1; :: thesis: verum