let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

let X be ManySortedSet of the carrier of S; :: thesis: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

assume (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A1: x in (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] by XBOOLE_0:def 1;

x in Union (coprod X) by A1, XBOOLE_0:def 4;

then x in union (rng (coprod X)) by CARD_3:def 4;

then consider A being set such that

A2: x in A and

A3: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A4: s in dom (coprod X) and

A5: (coprod X) . s = A by A3, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A4;

A = coprod (s,X) by A5, Def3;

then A6: ex a being set st

( a in X . s & x = [a,s] ) by A2, Def2;

x in [: the carrier' of S,{ the carrier of S}:] by A1, XBOOLE_0:def 4;

then s in { the carrier of S} by A6, ZFMISC_1:87;

then ( s in the carrier of S & s = the carrier of S ) by TARSKI:def 1;

hence contradiction ; :: thesis: verum

let X be ManySortedSet of the carrier of S; :: thesis: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

assume (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A1: x in (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] by XBOOLE_0:def 1;

x in Union (coprod X) by A1, XBOOLE_0:def 4;

then x in union (rng (coprod X)) by CARD_3:def 4;

then consider A being set such that

A2: x in A and

A3: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A4: s in dom (coprod X) and

A5: (coprod X) . s = A by A3, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A4;

A = coprod (s,X) by A5, Def3;

then A6: ex a being set st

( a in X . s & x = [a,s] ) by A2, Def2;

x in [: the carrier' of S,{ the carrier of S}:] by A1, XBOOLE_0:def 4;

then s in { the carrier of S} by A6, ZFMISC_1:87;

then ( s in the carrier of S & s = the carrier of S ) by TARSKI:def 1;

hence contradiction ; :: thesis: verum