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 <> {} )

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

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
(coprod X) . i <> {}
; :: thesis: X . i <> {}
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;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

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