theorem Th60: :: MSAFREE4:60

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )