theorem Th24: :: MSAFREE3:24

for S being non void Signature
for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0})))