theorem Th135: :: MSAFREE5:144

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for h being Endomorphism of Free (S,X) holds
( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )