theorem :: ABCMIZ_1:125

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