now

let x be set ; :: thesis: ( x in I implies not (coprod X) . x is empty )
assume x in I ; :: thesis: not (coprod X) . x is empty
then reconsider i = x as Element of I ;
consider a being set such that
A1: a in X . i by XBOOLE_0:def 1;
(coprod X) . i = coprod (i,X) by Def3;
then [a,i] in (coprod X) . i by A1, Def2;
hence not (coprod X) . x is empty ; :: thesis: verum

end;

hence coprod X is non-empty by PBOOLE:def 16; :: thesis: verum