theorem Lem9: :: MSAFREE5:133

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 xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2