theorem Th60: :: MSAFREE5:123

for S being non empty non void ManySortedSign
for s, s1 being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for C being context of x st X is non-trivial & the_sort_of C = s1 holds
for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)