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