theorem Th4: :: FACIRC_2:4

for x being set
for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)