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