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

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