support f c= dom f by Def10;
hence support f is Subset of X by FUNCT_2:def 1; :: thesis: verum