Support f c= dom f by Def3;
hence Support f is Subset of X by XBOOLE_1:1; :: thesis: verum