theorem Th4: :: MSAFREE:4

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