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