for S being non empty non void ManySortedSign
for Y being infinite-yielding ManySortedSet of the carrier of S
for v, v1 being Element of (Free (S,Y))
for h being Endomorphism of Free (S,Y)
for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) holds
h . v = v1