for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z
for w, p being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p