theorem Th17: :: MSAFREE3:17

for S being non void Signature
for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds
( the_sort_of t = s & variables_in t c= X )