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 ;
A1: (coprod X) . i = coprod i,X by Def3;
consider a being set such that
A2: a in X . i by XBOOLE_0:def 1;
[a,i] in (coprod X) . i by A1, A2, Def2;
hence not (coprod X) . x is empty ; :: thesis: verum

end;

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