consider x being object such that
A1: ( x in dom f & not f . x is empty ) by FUNCT_1:def 8;
not [:(f . x),{x}:] is empty by A1;
then not (disjoin f) . x is empty by A1, CARD_3:def 3;
hence not disjoin f is empty-yielding ; :: thesis: verum