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 set 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 set such that
A4: s in dom (coprod X) and
A5: (coprod X) . s = A by A3, FUNCT_1:def 5;
reconsider s = s as SortSymbol of S by A4, PARTFUN1:def 4;
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:106;
then ( s in the carrier of S & s = the carrier of S ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum