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