dom X = I by PARTFUN1:def 4;
hence ( X is empty-yielding iff for i being set st i in I holds
X . i is empty ) by FUNCT_1:def 14; :: thesis: verum