dom f = X by FUNCT_2:def 1;
then not (dom f) /\ A is empty by XBOOLE_1:28;
then dom f meets A ;
hence not f | A is empty by RELAT_1:66; :: thesis: verum