theorem Th32: :: MSAFREE3:32

for S being non void Signature
for Y being non-empty ManySortedSet of the carrier of S
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t