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

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