theorem Th124: :: ABCMIZ_1:124

for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being set st t in Union the Sorts of (Free (S,X)) holds
t is Term of S,(X (\/) ( the carrier of S --> {0}))