theorem Th23: :: MSAFREE3:23

for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being Term of S,(X (\/) ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s