let I be set ; :: thesis: for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
let X be ManySortedSet of I; :: thesis: for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
let i be set ; :: thesis: ( i in I implies ( X . i <> {} iff (coprod X) . i <> {} ) )
assume A1: i in I ; :: thesis: ( X . i <> {} iff (coprod X) . i <> {} )
then A2: (coprod X) . i = coprod (i,X) by Def3;
thus ( X . i <> {} implies (coprod X) . i <> {} ) :: thesis: ( (coprod X) . i <> {} implies X . i <> {} )

proof

assume X . i <> {} ; :: thesis: (coprod X) . i <> {}
then consider x being object such that
A3: x in X . i by XBOOLE_0:def 1;
[x,i] in (coprod X) . i by A1, A2, A3, Def2;
hence (coprod X) . i <> {} ; :: thesis: verum

end;

assume (coprod X) . i <> {} ; :: thesis: X . i <> {}
then consider a being object such that
A4: a in coprod (i,X) by A2, XBOOLE_0:def 1;
ex x being set st
( x in X . i & a = [x,i] ) by A1, A4, Def2;
hence X . i <> {} ; :: thesis: verum