theorem :: MSAFREE3:35

for x being set
for S being non void Signature
for X being empty-yielding ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )