for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds
(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting