set i = the Element of I;
consider a being object such that
A1: a in X . the Element of I by XBOOLE_0:def 1;
dom X = I by PARTFUN1:def 2;
then X . the Element of I in rng X by FUNCT_1:def 3;
then a in union (rng X) by A1, TARSKI:def 4;
hence not Union X is empty by CARD_3:def 4; :: thesis: verum