theorem Th42: :: MSAFREE5:85

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 w being Element of Args (o,(Free (S,Z)))
for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))