theorem Th59: :: MSAFREE5:119

for m being Element of NAT
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for q being Element of Args (o,(Free (S,Y)))
for V being finite set st m in dom q & (the_arity_of o) /. m = s holds
ex y being Element of Y . s ex C1 being context of y ex q1 being Element of Args (o,(Free (S,Y))) st
( y nin V & C1 = o -term q1 & q1 = q +* (m,(y -term)) & q1 is y -context_including & m = y -context_pos_in q1 & y -context_in q1 = y -term )