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