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;
A2: ( x in Union (coprod X) & x in [:the carrier' of S,{the carrier of S}:] ) 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
A3: ( x in A & A in rng (coprod X) ) by TARSKI:def 4;
consider s being set such that
A4: ( s in dom (coprod X) & (coprod X) . s = A ) by A3, FUNCT_1:def 5;
reconsider s = s as SortSymbol of S by A4, PBOOLE:def 3;
A5: s in the carrier of S ;
A = coprod s,X by A4, Def3;
then consider a being set such that
A6: ( a in X . s & x = [a,s] ) by A3, Def2;
s in {the carrier of S} by A2, A6, ZFMISC_1:106;
then s = the carrier of S by TARSKI:def 1;
hence contradiction by A5; :: thesis: verum