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