theorem Th8: :: MSAFREE3:8

for S being non void Signature
for X being empty-yielding ManySortedSet of the carrier of S
for x being Element of (Free (S,X)) holds x is Term of S,(X (\/) ( the carrier of S --> {0}))